Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-12 15:40:01 -0700 (Mon, 12 Oct 1998)
Revision: 2493
Log message:

      Added "reflection" theory, for reflecting sentences in the meta-logic
      into the Nuprl type theory.
      

Changes	Path
+4 -0	metaprl/editor/ml/Makefile
+1 -1	metaprl/editor/ml/nl
+0 -1	metaprl/editor/ml/x.ml
+7 -15	metaprl/editor/ml/y.ml
+25 -4	metaprl/refiner/refiner/refine.mlp
+8 -4	metaprl/refiner/refsig/refine_sig.ml
+6 -4	metaprl/theories/itt/itt_bool.ml
+6 -4	metaprl/theories/itt/itt_bool.mli
+15 -4	metaprl/theories/itt/itt_int.ml
+8 -4	metaprl/theories/itt/itt_int.mli
+55 -13	metaprl/theories/itt/itt_list.ml
+13 -4	metaprl/theories/itt/itt_list.mli
+17 -12	metaprl/theories/itt/itt_prod.ml
+6 -4	metaprl/theories/itt/itt_theory.ml
Properties	metaprl/theories/reflect_itt
Added	metaprl/theories/reflect_itt/Makefile
Properties	metaprl/theories/reflect_itt/Makefile
Added	metaprl/theories/reflect_itt/refl_term.ml
Properties	metaprl/theories/reflect_itt/refl_term.ml
Added	metaprl/theories/reflect_itt/refl_term.mli
Properties	metaprl/theories/reflect_itt/refl_term.mli
Binary	metaprl/theories/reflect_itt/refl_term.prlb
Properties	metaprl/theories/reflect_itt/refl_term.prlb
+25 -11	metaprl/theories/tactic/rewrite_type.ml