Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-17 21:52:00 -0800 (Mon, 17 Nov 2003)
Revision: 5110
Log message:

      
      Some proofs in mesa theory.
      The proof of
      /nuprl_ring__leader1_object_directory/nuprl_ring__leader1__compatible
      takes 10 minutes in Nuprl and only 5 sec in Metaprl.
      (Measurement was done on differnt machines, but still impressive).
      

Changes  Path
Properties metaprl/theories/mesa
+42 -0 metaprl/theories/mesa/ma_event__systems.ml
+4 -0 metaprl/theories/mesa/ma_event__systems.mli
+5 -0 metaprl/theories/mesa/ma_message__automata.ml
Added metaprl/theories/mesa/ma_message__automata.prla
Properties metaprl/theories/mesa/ma_message__automata.prla
Added metaprl/theories/mesa/nuprl_Dconstant_object_directory.prla
Properties metaprl/theories/mesa/nuprl_Dconstant_object_directory.prla
+0 -0 metaprl/theories/mesa/nuprl_general__theory.ml
Added metaprl/theories/mesa/nuprl_once_object_directory.prla
Properties metaprl/theories/mesa/nuprl_once_object_directory.prla
Added metaprl/theories/mesa/nuprl_recognizer1_object_directory.prla
Properties metaprl/theories/mesa/nuprl_recognizer1_object_directory.prla
Added metaprl/theories/mesa/nuprl_ring__leader1_object_directory.prla
Properties metaprl/theories/mesa/nuprl_ring__leader1_object_directory.prla
Added metaprl/theories/mesa/nuprl_send__once_object_directory.prla
Properties metaprl/theories/mesa/nuprl_send__once_object_directory.prla
Added metaprl/theories/mesa/nuprl_trigger1_object_directory.prla
Properties metaprl/theories/mesa/nuprl_trigger1_object_directory.prla