Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-09-06 17:44:30 -0700 (Mon, 06 Sep 1999)
Revision: 2812
Log message:

      Finally fixed the tutorial so that we have a derivation of
      classical first-order logic.  The HTML docs are not yet up-to-date.
      

Changes  Path
+24 -0 metaprl/filter/filter/filter_parse.ml
+16 -5 metaprl/theories/fol/Makefile
Added metaprl/theories/fol/cfol_itt_all.ml
Properties metaprl/theories/fol/cfol_itt_all.ml
Added metaprl/theories/fol/cfol_itt_all.mli
Properties metaprl/theories/fol/cfol_itt_all.mli
Added metaprl/theories/fol/cfol_itt_all.prla
Properties metaprl/theories/fol/cfol_itt_all.prla
Added metaprl/theories/fol/cfol_itt_and.ml
Properties metaprl/theories/fol/cfol_itt_and.ml
Added metaprl/theories/fol/cfol_itt_and.mli
Properties metaprl/theories/fol/cfol_itt_and.mli
Added metaprl/theories/fol/cfol_itt_and.prla
Properties metaprl/theories/fol/cfol_itt_and.prla
Added metaprl/theories/fol/cfol_itt_base.ml
Properties metaprl/theories/fol/cfol_itt_base.ml
Added metaprl/theories/fol/cfol_itt_base.mli
Properties metaprl/theories/fol/cfol_itt_base.mli
Added metaprl/theories/fol/cfol_itt_base.prla
Properties metaprl/theories/fol/cfol_itt_base.prla
Added metaprl/theories/fol/cfol_magic.ml
Properties metaprl/theories/fol/cfol_magic.ml
Added metaprl/theories/fol/cfol_magic.mli
Properties metaprl/theories/fol/cfol_magic.mli
Added metaprl/theories/fol/cfol_magic.prla
Properties metaprl/theories/fol/cfol_magic.prla
Added metaprl/theories/fol/cfol_theory.ml
Properties metaprl/theories/fol/cfol_theory.ml
Added metaprl/theories/fol/cfol_theory.mli
Properties metaprl/theories/fol/cfol_theory.mli
Added metaprl/theories/fol/cfol_theory.prla
Properties metaprl/theories/fol/cfol_theory.prla
+5 -10 metaprl/theories/fol/fol_all.ml
+2 -1 metaprl/theories/fol/fol_all.mli
Added metaprl/theories/fol/fol_all.prla
Properties metaprl/theories/fol/fol_all.prla
+2 -3 metaprl/theories/fol/fol_and.ml
Added metaprl/theories/fol/fol_and.prla
Properties metaprl/theories/fol/fol_and.prla
Deleted metaprl/theories/fol/fol_class.ml
Deleted metaprl/theories/fol/fol_class.mli
+5 -7 metaprl/theories/fol/fol_exists.ml
+1 -1 metaprl/theories/fol/fol_exists.mli
Added metaprl/theories/fol/fol_exists.prla
Properties metaprl/theories/fol/fol_exists.prla
+10 -5 metaprl/theories/fol/fol_false.ml
Added metaprl/theories/fol/fol_false.prla
Properties metaprl/theories/fol/fol_false.prla
+1 -3 metaprl/theories/fol/fol_implies.ml
Added metaprl/theories/fol/fol_implies.prla
Properties metaprl/theories/fol/fol_implies.prla
Added metaprl/theories/fol/fol_itt_and.ml
Properties metaprl/theories/fol/fol_itt_and.ml
Added metaprl/theories/fol/fol_itt_and.mli
Properties metaprl/theories/fol/fol_itt_and.mli
Added metaprl/theories/fol/fol_itt_and.prla
Properties metaprl/theories/fol/fol_itt_and.prla
Added metaprl/theories/fol/fol_itt_false.ml
Properties metaprl/theories/fol/fol_itt_false.ml
Added metaprl/theories/fol/fol_itt_false.mli
Properties metaprl/theories/fol/fol_itt_false.mli
Added metaprl/theories/fol/fol_itt_false.prla
Properties metaprl/theories/fol/fol_itt_false.prla
Added metaprl/theories/fol/fol_itt_implies.ml
Properties metaprl/theories/fol/fol_itt_implies.ml
Added metaprl/theories/fol/fol_itt_implies.mli
Properties metaprl/theories/fol/fol_itt_implies.mli
Added metaprl/theories/fol/fol_itt_implies.prla
Properties metaprl/theories/fol/fol_itt_implies.prla
Added metaprl/theories/fol/fol_itt_or.ml
Properties metaprl/theories/fol/fol_itt_or.ml
Added metaprl/theories/fol/fol_itt_or.mli
Properties metaprl/theories/fol/fol_itt_or.mli
Added metaprl/theories/fol/fol_itt_or.prla
Properties metaprl/theories/fol/fol_itt_or.prla
Added metaprl/theories/fol/fol_itt_prop.ml
Properties metaprl/theories/fol/fol_itt_prop.ml
Added metaprl/theories/fol/fol_itt_prop.mli
Properties metaprl/theories/fol/fol_itt_prop.mli
Added metaprl/theories/fol/fol_itt_prop.prla
Properties metaprl/theories/fol/fol_itt_prop.prla
Added metaprl/theories/fol/fol_itt_true.ml
Properties metaprl/theories/fol/fol_itt_true.ml
Added metaprl/theories/fol/fol_itt_true.mli
Properties metaprl/theories/fol/fol_itt_true.mli
Added metaprl/theories/fol/fol_itt_true.prla
Properties metaprl/theories/fol/fol_itt_true.prla
Added metaprl/theories/fol/fol_itt_type.ml
Properties metaprl/theories/fol/fol_itt_type.ml
Added metaprl/theories/fol/fol_itt_type.mli
Properties metaprl/theories/fol/fol_itt_type.mli
Added metaprl/theories/fol/fol_itt_type.prla
Properties metaprl/theories/fol/fol_itt_type.prla
+0 -2 metaprl/theories/fol/fol_not.ml
Added metaprl/theories/fol/fol_not.prla
Properties metaprl/theories/fol/fol_not.prla
+0 -3 metaprl/theories/fol/fol_or.ml
Added metaprl/theories/fol/fol_or.prla
Properties metaprl/theories/fol/fol_or.prla
Added metaprl/theories/fol/fol_pred.ml
Properties metaprl/theories/fol/fol_pred.ml
Added metaprl/theories/fol/fol_pred.mli
Properties metaprl/theories/fol/fol_pred.mli
Added metaprl/theories/fol/fol_pred.prla
Properties metaprl/theories/fol/fol_pred.prla
Added metaprl/theories/fol/fol_prop.ml
Properties metaprl/theories/fol/fol_prop.ml
Added metaprl/theories/fol/fol_prop.mli
Properties metaprl/theories/fol/fol_prop.mli
Added metaprl/theories/fol/fol_prop.prla
Properties metaprl/theories/fol/fol_prop.prla
+3 -9 metaprl/theories/fol/fol_struct.ml
+3 -3 metaprl/theories/fol/fol_struct.mli
Added metaprl/theories/fol/fol_struct.prla
Properties metaprl/theories/fol/fol_struct.prla
+53 -6 metaprl/theories/fol/fol_theory.ml
+41 -4 metaprl/theories/fol/fol_theory.mli
Added metaprl/theories/fol/fol_theory.prla
Properties metaprl/theories/fol/fol_theory.prla
+0 -2 metaprl/theories/fol/fol_true.ml
Added metaprl/theories/fol/fol_true.prla
Properties metaprl/theories/fol/fol_true.prla
+35 -44 metaprl/theories/fol/fol_type.ml
+31 -9 metaprl/theories/fol/fol_type.mli
Added metaprl/theories/fol/fol_type.prla
Properties metaprl/theories/fol/fol_type.prla
+1 -0 metaprl/theories/itt/Makefile
+1 -1 metaprl/theories/itt/itt_equal.ml
Added metaprl/theories/itt/itt_esquash.ml
Properties metaprl/theories/itt/itt_esquash.ml
Added metaprl/theories/itt/itt_esquash.mli
Properties metaprl/theories/itt/itt_esquash.mli
Added metaprl/theories/itt/itt_esquash.prla
Properties metaprl/theories/itt/itt_esquash.prla
+4 -0 metaprl/theories/itt/itt_prod.ml
+32 -21 metaprl/theories/itt/itt_quotient.ml
+1 -1 metaprl/theories/itt/itt_quotient.mli
+12 -0 metaprl/theories/itt/itt_set.ml
+1 -0 metaprl/theories/itt/itt_set.mli
+4 -1 metaprl/theories/itt/itt_theory.ml
+1 -0 metaprl/theories/itt/itt_theory.mli
+1 -1 metaprl/theories/tactic/nuprl_font.ml
Properties metaprl/theories/tutorial
Added metaprl/theories/tutorial/Makefile
Properties metaprl/theories/tutorial/Makefile