Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-22 12:27:15 -0800 (Sat, 22 Jan 2005)
Revision: 6471
Log message:

      - sequent_arg is no longer used except in the 0-arity form.
      - All proofs now replay without opname hacks.
      

Changes  Path
+5 -14 metaprl-branches/opname_classes2/filter/base/filter_cache_fun.ml
+1 -1 metaprl-branches/opname_classes2/filter/base/filter_magic.ml
+2 -2 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+8 -34 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+16 -11 metaprl-branches/opname_classes2/refiner/refbase/opname.ml
+77 -10 metaprl-branches/opname_classes2/refiner/reflib/ascii_io.ml
+5 -2 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+2 -1 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.mli
+7 -7 metaprl-branches/opname_classes2/support/display/perv.ml
+7 -4 metaprl-branches/opname_classes2/support/display/perv.mli
+6 -3 metaprl-branches/opname_classes2/support/display/summary.ml
+4 -1 metaprl-branches/opname_classes2/support/display/summary.mli
+3 -6 metaprl-branches/opname_classes2/theories/base/base_meta.ml
+0 -1 metaprl-branches/opname_classes2/theories/base/base_meta.mli
+1 -2 metaprl-branches/opname_classes2/theories/base/base_reflection.ml
+1 -2 metaprl-branches/opname_classes2/theories/base/base_reflection.mli
+2 -2 metaprl-branches/opname_classes2/theories/cic/cic_ind_cases.ml
+1 -6 metaprl-branches/opname_classes2/theories/cic/cic_lambda.ml
+0 -3 metaprl-branches/opname_classes2/theories/cic/cic_lambda.mli
+105 -104 metaprl-branches/opname_classes2/theories/itt/OMakefile
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_algebra_df.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_atom.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_bintree.ml
+81 -28 metaprl-branches/opname_classes2/theories/itt/itt_bintree.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_closure.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_closure.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_cyclic_group.ml
+51 -0 metaprl-branches/opname_classes2/theories/itt/itt_cyclic_group.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_datatree.ml
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_field2.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_field2.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_field_e.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_field_e.prla
+2 -2 metaprl-branches/opname_classes2/theories/itt/itt_fun.ml
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_fun.mli
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_group.ml
+52 -0 metaprl-branches/opname_classes2/theories/itt/itt_group.prla
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_grouplikeobj.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_grouplikeobj.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_intdomain.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_intdomain.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_intdomain_e.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_intdomain_e.prla
Added metaprl-branches/opname_classes2/theories/itt/itt_labels.mlz
Properties metaprl-branches/opname_classes2/theories/itt/itt_labels.mlz
+54 -0 metaprl-branches/opname_classes2/theories/itt/itt_mpoly.prla
+54 -0 metaprl-branches/opname_classes2/theories/itt/itt_mpoly2.prla
+54 -0 metaprl-branches/opname_classes2/theories/itt/itt_mpoly2_bench.prla
+54 -0 metaprl-branches/opname_classes2/theories/itt/itt_mpoly3.prla
+54 -0 metaprl-branches/opname_classes2/theories/itt/itt_mpoly3_bench.prla
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_obj_base_rewrite.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_obj_base_rewrite.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_order.ml
+51 -0 metaprl-branches/opname_classes2/theories/itt/itt_order.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_poly.ml
+50 -0 metaprl-branches/opname_classes2/theories/itt/itt_poly.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_quotient_group.ml
+52 -0 metaprl-branches/opname_classes2/theories/itt/itt_quotient_group.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_rat.ml
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_rat.mli
+51 -0 metaprl-branches/opname_classes2/theories/itt/itt_rat.prla
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_rbtree.ml
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_record.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_record.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_record_exm.ml
+73 -20 metaprl-branches/opname_classes2/theories/itt/itt_record_exm.prla
+59 -5 metaprl-branches/opname_classes2/theories/itt/itt_record_label.prla
+2 -1 metaprl-branches/opname_classes2/theories/itt/itt_record_renaming.ml
+57 -4 metaprl-branches/opname_classes2/theories/itt/itt_record_renaming.prla
+2035 -1883 metaprl-branches/opname_classes2/theories/itt/itt_reflection.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_relation_str.ml
+2 -2 metaprl-branches/opname_classes2/theories/itt/itt_ring2.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_ring2.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_ring_e.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_ring_e.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_ring_uce.ml
+52 -0 metaprl-branches/opname_classes2/theories/itt/itt_ring_uce.prla
+3 -2 metaprl-branches/opname_classes2/theories/itt/itt_set_str.ml
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_sortedtree.ml
+66 -14 metaprl-branches/opname_classes2/theories/itt/itt_sortedtree.prla
+1 -0 metaprl-branches/opname_classes2/theories/itt/itt_unitring.ml
+53 -0 metaprl-branches/opname_classes2/theories/itt/itt_unitring.prla
+2 -15 metaprl-branches/opname_classes2/theories/phobos/phobos_theory.ml
+1 -1 metaprl-branches/opname_classes2/theories/tptp/tptp.ml
+7001 -8113 metaprl-branches/opname_classes2/theories/tptp/tptp.prla
+0 -0 metaprl-branches/opname_classes2/util/check-status
+2 -2 metaprl-branches/opname_classes2/util/check-status.sh