Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-01 20:01:07 -0800 (Tue, 01 Nov 2005)
Revision: 8075
Log message:

      Rebuilt the FSub languages directly from BTerm.
      I think this is the way to go, the theories are much smaller.
      

Changes  Path
+10 -0 metaprl/theories/itt/core/itt_decidable.mli
+27 -0 metaprl/theories/itt/reflection/core/itt_hoas_operator.ml
+2 -0 metaprl/theories/itt/reflection/core/itt_hoas_operator.mli
+1 -0 metaprl/theories/poplmark/naive/OMakefile
+40 -0 metaprl/theories/poplmark/naive/pmn_core_judgments.ml
+149 -736 metaprl/theories/poplmark/naive/pmn_core_terms.ml
+1 -6 metaprl/theories/poplmark/naive/pmn_core_terms.mli
+5581 -9009 metaprl/theories/poplmark/naive/pmn_core_terms.prla
Copied metaprl/theories/poplmark/naive/pmn_core_terms_old.ml
Copied metaprl/theories/poplmark/naive/pmn_core_terms_old.mli
Copied metaprl/theories/poplmark/naive/pmn_core_terms_old.prla