Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 00:42:49 -0700 (Wed, 07 May 2003)
Revision: 4570
Log message:

      - Sequent args are now parsed int a term with a "sequent_arg" opname,
      not an xlist term
      - Restored the code for "dfrom_depth" debugging
      - Fixed an unballanced display form for ifthenelse in Ocaml_expr_df
      

Changes  Path
+28 -21 metaprl/filter/filter/term_grammar.ml
+1 -1 metaprl/mk/preface
+7 -1 metaprl/refiner/reflib/dform.ml
+1 -2 metaprl/refiner/reflib/rformat.ml
+40 -40 metaprl/support/display/base_dform.ml
+3 -3 metaprl/support/display/ocaml_expr_df.ml
+5 -5 metaprl/support/shell/shell_rewrite.ml
+24 -11 metaprl/theories/base/base_rewrite.ml
+6 -6 metaprl/theories/base/base_rewrite.mli
+8 -4 metaprl/theories/base/base_rewrite.prla
+0 -1 metaprl/theories/base/base_trivial.ml
+0 -1 metaprl/theories/base/base_trivial.mli
+6 -6 metaprl/theories/czf/czf_itt_abel_group.ml
+9 -5 metaprl/theories/czf/czf_itt_abel_group.prla
+16 -16 metaprl/theories/czf/czf_itt_all.ml
+60 -56 metaprl/theories/czf/czf_itt_all.prla
+16 -16 metaprl/theories/czf/czf_itt_and.ml
+42 -38 metaprl/theories/czf/czf_itt_and.prla
+19 -19 metaprl/theories/czf/czf_itt_axioms.ml
+290 -286 metaprl/theories/czf/czf_itt_axioms.prla
+422 -422 metaprl/theories/czf/czf_itt_bool.ml
+1049 -1045 metaprl/theories/czf/czf_itt_bool.prla
+1 -1 metaprl/theories/czf/czf_itt_comment.prla
+60 -60 metaprl/theories/czf/czf_itt_coset.ml
+57 -53 metaprl/theories/czf/czf_itt_coset.prla
+32 -32 metaprl/theories/czf/czf_itt_cyclic_group.ml
+106 -102 metaprl/theories/czf/czf_itt_cyclic_group.prla
+28 -28 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+34 -30 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+20 -20 metaprl/theories/czf/czf_itt_dall.ml
+206 -202 metaprl/theories/czf/czf_itt_dall.prla
+21 -21 metaprl/theories/czf/czf_itt_dexists.ml
+118 -114 metaprl/theories/czf/czf_itt_dexists.prla
+2 -2 metaprl/theories/czf/czf_itt_empty.ml
+6 -2 metaprl/theories/czf/czf_itt_empty.prla
+57 -57 metaprl/theories/czf/czf_itt_eq.ml
+342 -338 metaprl/theories/czf/czf_itt_eq.prla
+213 -213 metaprl/theories/czf/czf_itt_equiv.ml
+437 -433 metaprl/theories/czf/czf_itt_equiv.prla
+16 -16 metaprl/theories/czf/czf_itt_exists.ml
+48 -44 metaprl/theories/czf/czf_itt_exists.prla
+4 -4 metaprl/theories/czf/czf_itt_false.ml
+4 -4 metaprl/theories/czf/czf_itt_false.mli
+8 -4 metaprl/theories/czf/czf_itt_false.prla
+201 -201 metaprl/theories/czf/czf_itt_group.ml
+154 -150 metaprl/theories/czf/czf_itt_group.prla
+25 -25 metaprl/theories/czf/czf_itt_group_bvd.ml
+65 -61 metaprl/theories/czf/czf_itt_group_bvd.prla
+35 -35 metaprl/theories/czf/czf_itt_group_power.ml
+374 -370 metaprl/theories/czf/czf_itt_group_power.prla
+74 -74 metaprl/theories/czf/czf_itt_hom.ml
+524 -520 metaprl/theories/czf/czf_itt_hom.prla
+24 -24 metaprl/theories/czf/czf_itt_implies.ml
+50 -46 metaprl/theories/czf/czf_itt_implies.prla
+42 -38 metaprl/theories/czf/czf_itt_infinity.prla
+17 -17 metaprl/theories/czf/czf_itt_inv_image.ml
+23 -19 metaprl/theories/czf/czf_itt_inv_image.prla
+33 -33 metaprl/theories/czf/czf_itt_isect.ml
+54 -50 metaprl/theories/czf/czf_itt_isect.prla
+11 -11 metaprl/theories/czf/czf_itt_iso.ml
+61 -57 metaprl/theories/czf/czf_itt_iso.prla
+83 -83 metaprl/theories/czf/czf_itt_ker.ml
+580 -576 metaprl/theories/czf/czf_itt_ker.prla
+71 -71 metaprl/theories/czf/czf_itt_kleingroup.ml
+378 -374 metaprl/theories/czf/czf_itt_kleingroup.prla
+34 -34 metaprl/theories/czf/czf_itt_member.ml
+176 -172 metaprl/theories/czf/czf_itt_member.prla
+37 -37 metaprl/theories/czf/czf_itt_nat.ml
+237 -233 metaprl/theories/czf/czf_itt_nat.prla
+13 -13 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+62 -58 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+16 -16 metaprl/theories/czf/czf_itt_or.ml
+39 -35 metaprl/theories/czf/czf_itt_or.prla
+22 -22 metaprl/theories/czf/czf_itt_pair.ml
+30 -26 metaprl/theories/czf/czf_itt_pair.prla
+11 -11 metaprl/theories/czf/czf_itt_power.ml
+190 -186 metaprl/theories/czf/czf_itt_power.prla
+4 -4 metaprl/theories/czf/czf_itt_rel.ml
+9 -5 metaprl/theories/czf/czf_itt_rel.prla
+7 -7 metaprl/theories/czf/czf_itt_sall.ml
+7 -7 metaprl/theories/czf/czf_itt_sall.mli
+15 -11 metaprl/theories/czf/czf_itt_sall.prla
+28 -28 metaprl/theories/czf/czf_itt_sep.ml
+235 -231 metaprl/theories/czf/czf_itt_sep.prla
+25 -25 metaprl/theories/czf/czf_itt_set.ml
+20 -20 metaprl/theories/czf/czf_itt_set.mli
+86 -82 metaprl/theories/czf/czf_itt_set.prla
+20 -20 metaprl/theories/czf/czf_itt_set_bvd.ml
+86 -82 metaprl/theories/czf/czf_itt_set_bvd.prla
+18 -18 metaprl/theories/czf/czf_itt_set_ind.ml
+18 -18 metaprl/theories/czf/czf_itt_set_ind.mli
+299 -295 metaprl/theories/czf/czf_itt_set_ind.prla
+19 -19 metaprl/theories/czf/czf_itt_setdiff.ml
+37 -33 metaprl/theories/czf/czf_itt_setdiff.prla
+8 -8 metaprl/theories/czf/czf_itt_sexists.ml
+14 -10 metaprl/theories/czf/czf_itt_sexists.prla
+10 -10 metaprl/theories/czf/czf_itt_singleton.ml
+49 -45 metaprl/theories/czf/czf_itt_singleton.prla
+48 -48 metaprl/theories/czf/czf_itt_subgroup.ml
+130 -126 metaprl/theories/czf/czf_itt_subgroup.prla
+19 -19 metaprl/theories/czf/czf_itt_subset.ml
+27 -23 metaprl/theories/czf/czf_itt_subset.prla
+4 -4 metaprl/theories/czf/czf_itt_true.ml
+4 -4 metaprl/theories/czf/czf_itt_true.mli
+8 -4 metaprl/theories/czf/czf_itt_true.prla
+34 -34 metaprl/theories/czf/czf_itt_union.ml
+311 -307 metaprl/theories/czf/czf_itt_union.prla
+2 -2 metaprl/theories/experimental/compile/m_cps.ml
+2 -2 metaprl/theories/experimental/compile/m_ir.ml
+1 -1 metaprl/theories/experimental/compile/m_ir.mli
+4 -4 metaprl/theories/experimental/compile/m_standardize.ml
+4 -4 metaprl/theories/experimental/compile/m_test.ml
+2 -2 metaprl/theories/experimental/compile/m_x86_codegen.ml
+4 -5 metaprl/theories/fir/mfir_sequent.ml
+1 -1 metaprl/theories/fir/mfir_sequent.mli
+26 -26 metaprl/theories/fir/mfir_test.ml
+22 -24 metaprl/theories/fir/mfir_test.prla
+42 -42 metaprl/theories/fir/mfir_tr_atom.ml
+26 -26 metaprl/theories/fir/mfir_tr_base.ml
+100 -100 metaprl/theories/fir/mfir_tr_exp.ml
+23 -23 metaprl/theories/fir/mfir_tr_store.ml
+64 -64 metaprl/theories/fir/mfir_tr_types.ml
+9 -9 metaprl/theories/fol/cfol_itt_all.ml
+46 -42 metaprl/theories/fol/cfol_itt_all.prla
+13 -13 metaprl/theories/fol/cfol_itt_and.ml
+112 -108 metaprl/theories/fol/cfol_itt_and.prla
+19 -19 metaprl/theories/fol/cfol_itt_base.ml
+45 -41 metaprl/theories/fol/cfol_itt_base.prla
+2 -2 metaprl/theories/fol/cfol_magic.ml
+9 -9 metaprl/theories/fol/fol_all.ml
+8 -8 metaprl/theories/fol/fol_all_itt.ml
+10 -10 metaprl/theories/fol/fol_and.ml
+6 -6 metaprl/theories/fol/fol_bisect_itt.ml
+4 -4 metaprl/theories/fol/fol_ctheory.ml
+14 -10 metaprl/theories/fol/fol_ctheory.prla
+8 -8 metaprl/theories/fol/fol_exists.ml
+2 -2 metaprl/theories/fol/fol_false.ml
+1 -1 metaprl/theories/fol/fol_false.mli
+9 -9 metaprl/theories/fol/fol_implies.ml
+8 -8 metaprl/theories/fol/fol_itt_and.ml
+24 -20 metaprl/theories/fol/fol_itt_and.prla
+2 -2 metaprl/theories/fol/fol_itt_false.ml
+8 -4 metaprl/theories/fol/fol_itt_false.prla
+9 -9 metaprl/theories/fol/fol_itt_implies.ml
+21 -17 metaprl/theories/fol/fol_itt_implies.prla
+12 -12 metaprl/theories/fol/fol_itt_or.ml
+26 -22 metaprl/theories/fol/fol_itt_or.prla
+2 -2 metaprl/theories/fol/fol_itt_true.ml
+6 -2 metaprl/theories/fol/fol_itt_true.prla
+7 -7 metaprl/theories/fol/fol_not.ml
+13 -9 metaprl/theories/fol/fol_not.prla
+12 -12 metaprl/theories/fol/fol_or.ml
+1 -1 metaprl/theories/fol/fol_pred.ml
+20 -20 metaprl/theories/fol/fol_prop.ml
+43 -39 metaprl/theories/fol/fol_prop.prla
+6 -6 metaprl/theories/fol/fol_struct.ml
+2 -2 metaprl/theories/fol/fol_true.ml
+1 -1 metaprl/theories/fol/fol_univ.ml
+8 -8 metaprl/theories/fol/fol_univ_itt.ml
+71 -71 metaprl/theories/itt/ctt_markov.ml
+140 -136 metaprl/theories/itt/ctt_markov.prla
+13 -13 metaprl/theories/itt/itt_antiquotient.ml
+63 -59 metaprl/theories/itt/itt_antiquotient.prla
+7 -7 metaprl/theories/itt/itt_atom.ml
+5 -5 metaprl/theories/itt/itt_atom.mli
+7 -7 metaprl/theories/itt/itt_atom_bool.ml
+45 -45 metaprl/theories/itt/itt_bintree.ml
+53 -49 metaprl/theories/itt/itt_bintree.prla
+31 -31 metaprl/theories/itt/itt_bisect.ml
+76 -72 metaprl/theories/itt/itt_bisect.prla
+93 -93 metaprl/theories/itt/itt_bool.ml
+11 -11 metaprl/theories/itt/itt_bool.mli
+336 -332 metaprl/theories/itt/itt_bool.prla
+13 -9 metaprl/theories/itt/itt_bugs.prla
+21 -21 metaprl/theories/itt/itt_bunion.ml
+39 -35 metaprl/theories/itt/itt_bunion.prla
+173 -173 metaprl/theories/itt/itt_collection.ml
+164 -160 metaprl/theories/itt/itt_collection.prla
+74 -74 metaprl/theories/itt/itt_cyclic_group.ml
+725 -721 metaprl/theories/itt/itt_cyclic_group.prla
+22 -22 metaprl/theories/itt/itt_datatree.ml
+10 -10 metaprl/theories/itt/itt_decidable.ml
+12 -8 metaprl/theories/itt/itt_decidable.prla
+12 -12 metaprl/theories/itt/itt_derive.ml
+24 -20 metaprl/theories/itt/itt_derive.prla
+33 -33 metaprl/theories/itt/itt_dfun.ml
+29 -29 metaprl/theories/itt/itt_dfun.mli
+97 -93 metaprl/theories/itt/itt_dfun.prla
+42 -42 metaprl/theories/itt/itt_disect.ml
+3 -3 metaprl/theories/itt/itt_disect.mli
+116 -112 metaprl/theories/itt/itt_disect.prla
+29 -29 metaprl/theories/itt/itt_dprod.ml
+25 -25 metaprl/theories/itt/itt_dprod.mli
+31 -27 metaprl/theories/itt/itt_dprod.prla
+35 -35 metaprl/theories/itt/itt_dprod_imp.ml
+162 -158 metaprl/theories/itt/itt_dprod_imp.prla
+47 -42 metaprl/theories/itt/itt_equal.ml
+38 -38 metaprl/theories/itt/itt_equal.mli
+37 -33 metaprl/theories/itt/itt_equal.prla
+27 -27 metaprl/theories/itt/itt_esquash.ml
+34 -30 metaprl/theories/itt/itt_esquash.prla
+50 -50 metaprl/theories/itt/itt_example.ml
+2 -2 metaprl/theories/itt/itt_ext_equal.ml
+19 -15 metaprl/theories/itt/itt_ext_equal.prla
+417 -417 metaprl/theories/itt/itt_fset.ml
+17766 -18687 metaprl/theories/itt/itt_fset.prla
+32 -32 metaprl/theories/itt/itt_fun.ml
+27 -27 metaprl/theories/itt/itt_fun.mli
+47 -43 metaprl/theories/itt/itt_fun.prla
+394 -394 metaprl/theories/itt/itt_group.ml
+1913 -1909 metaprl/theories/itt/itt_group.prla
+84 -84 metaprl/theories/itt/itt_grouplikeobj.ml
+128 -124 metaprl/theories/itt/itt_grouplikeobj.prla
+64 -64 metaprl/theories/itt/itt_int_arith.ml
+1 -1 metaprl/theories/itt/itt_int_arith.mli
+109 -105 metaprl/theories/itt/itt_int_arith.prla
+120 -120 metaprl/theories/itt/itt_int_base.ml
+112 -112 metaprl/theories/itt/itt_int_base.mli
+220 -216 metaprl/theories/itt/itt_int_base.prla
+120 -120 metaprl/theories/itt/itt_int_ext.ml
+90 -90 metaprl/theories/itt/itt_int_ext.mli
+146 -142 metaprl/theories/itt/itt_int_ext.prla
+7 -7 metaprl/theories/itt/itt_inv_typing.ml
+53 -53 metaprl/theories/itt/itt_isect.ml
+26 -26 metaprl/theories/itt/itt_isect.mli
+75 -71 metaprl/theories/itt/itt_isect.prla
+31 -31 metaprl/theories/itt/itt_list.ml
+27 -27 metaprl/theories/itt/itt_list.mli
+83 -79 metaprl/theories/itt/itt_list.prla
+108 -108 metaprl/theories/itt/itt_list2.ml
+279 -275 metaprl/theories/itt/itt_list2.prla
+159 -159 metaprl/theories/itt/itt_logic.ml
+118 -114 metaprl/theories/itt/itt_logic.prla
+35 -35 metaprl/theories/itt/itt_nat.ml
+351 -347 metaprl/theories/itt/itt_nat.prla
+6 -6 metaprl/theories/itt/itt_pointwise.ml
+3 -3 metaprl/theories/itt/itt_pointwise.mli
+10 -6 metaprl/theories/itt/itt_pointwise.prla
+8 -8 metaprl/theories/itt/itt_pointwise2.ml
+18 -14 metaprl/theories/itt/itt_pointwise2.prla
+18 -18 metaprl/theories/itt/itt_prec.ml
+18 -18 metaprl/theories/itt/itt_prec.mli
+20 -20 metaprl/theories/itt/itt_prod.ml
+20 -20 metaprl/theories/itt/itt_prod.mli
+33 -29 metaprl/theories/itt/itt_prod.prla
+12 -12 metaprl/theories/itt/itt_prop_decide.ml
+58 -54 metaprl/theories/itt/itt_prop_decide.prla
+33 -33 metaprl/theories/itt/itt_quotient.ml
+33 -33 metaprl/theories/itt/itt_quotient.mli
+62 -58 metaprl/theories/itt/itt_quotient.prla
+15 -15 metaprl/theories/itt/itt_quotient_group.ml
+465 -461 metaprl/theories/itt/itt_quotient_group.prla
+33 -33 metaprl/theories/itt/itt_rbtree.ml
+110 -110 metaprl/theories/itt/itt_record.ml
+299 -295 metaprl/theories/itt/itt_record.prla
+53 -53 metaprl/theories/itt/itt_record0.ml
+260 -256 metaprl/theories/itt/itt_record0.prla
+37 -37 metaprl/theories/itt/itt_record_exm.ml
+379 -375 metaprl/theories/itt/itt_record_exm.prla
+12 -12 metaprl/theories/itt/itt_record_label.ml
+24 -20 metaprl/theories/itt/itt_record_label.prla
+18 -18 metaprl/theories/itt/itt_record_label0.ml
+5 -5 metaprl/theories/itt/itt_record_label0.mli
+76 -72 metaprl/theories/itt/itt_record_label0.prla
+22 -22 metaprl/theories/itt/itt_relation_str.ml
+49 -49 metaprl/theories/itt/itt_rfun.ml
+24 -24 metaprl/theories/itt/itt_rfun.mli
+62 -58 metaprl/theories/itt/itt_rfun.prla
+21 -21 metaprl/theories/itt/itt_set.ml
+18 -18 metaprl/theories/itt/itt_set.mli
+25 -21 metaprl/theories/itt/itt_set.prla
+20 -20 metaprl/theories/itt/itt_set_str.ml
+13 -13 metaprl/theories/itt/itt_singleton.ml
+35 -31 metaprl/theories/itt/itt_singleton.prla
+88 -88 metaprl/theories/itt/itt_sort.ml
+150 -146 metaprl/theories/itt/itt_sort.prla
+26 -26 metaprl/theories/itt/itt_sortedtree.ml
+452 -448 metaprl/theories/itt/itt_sortedtree.prla
+55 -134 metaprl/theories/itt/itt_squash.ml
+21 -33 metaprl/theories/itt/itt_squash.mli
+48 -44 metaprl/theories/itt/itt_squash.prla
+24 -24 metaprl/theories/itt/itt_squiggle.ml
+24 -20 metaprl/theories/itt/itt_squiggle.prla
+21 -21 metaprl/theories/itt/itt_srec.ml
+19 -19 metaprl/theories/itt/itt_srec.mli
+45 -45 metaprl/theories/itt/itt_struct.ml
+21 -21 metaprl/theories/itt/itt_struct.mli
+30 -26 metaprl/theories/itt/itt_struct.prla
+30 -30 metaprl/theories/itt/itt_struct2.ml
+103 -99 metaprl/theories/itt/itt_struct2.prla
+12 -12 metaprl/theories/itt/itt_struct3.ml
+12 -12 metaprl/theories/itt/itt_struct3.mli
+33 -29 metaprl/theories/itt/itt_struct3.prla
+62 -62 metaprl/theories/itt/itt_subset.ml
+37 -37 metaprl/theories/itt/itt_subset.mli
+111 -107 metaprl/theories/itt/itt_subset.prla
+35 -35 metaprl/theories/itt/itt_subset2.ml
+153 -149 metaprl/theories/itt/itt_subset2.prla
+33 -33 metaprl/theories/itt/itt_subtype.ml
+23 -23 metaprl/theories/itt/itt_subtype.mli
+31 -27 metaprl/theories/itt/itt_subtype.prla
+4 -4 metaprl/theories/itt/itt_test.ml
+10 -10 metaprl/theories/itt/itt_tsquash.ml
+17 -13 metaprl/theories/itt/itt_tsquash.prla
+24 -24 metaprl/theories/itt/itt_tunion.ml
+19 -19 metaprl/theories/itt/itt_tunion.mli
+65 -61 metaprl/theories/itt/itt_tunion.prla
+33 -33 metaprl/theories/itt/itt_union.ml
+31 -31 metaprl/theories/itt/itt_union.mli
+43 -39 metaprl/theories/itt/itt_union.prla
+4 -4 metaprl/theories/itt/itt_union2.ml
+9 -9 metaprl/theories/itt/itt_unit.ml
+9 -9 metaprl/theories/itt/itt_unit.mli
+13 -9 metaprl/theories/itt/itt_unit.prla
+5 -5 metaprl/theories/itt/itt_void.ml
+5 -5 metaprl/theories/itt/itt_void.mli
+10 -6 metaprl/theories/itt/itt_void.prla
+22 -22 metaprl/theories/itt/itt_w.ml
+22 -22 metaprl/theories/itt/itt_w.mli
+39 -35 metaprl/theories/itt/itt_w.prla
+10 -10 metaprl/theories/itt/itt_well_founded.ml
+76 -72 metaprl/theories/itt/itt_well_founded.prla
+47 -47 metaprl/theories/itt/jprover_tests.ml
+76 -76 metaprl/theories/sil/sil_itt_sos.ml
+28 -28 metaprl/theories/sil/sil_itt_state_types.ml
+33 -33 metaprl/theories/sil/sil_program.ml
+41 -41 metaprl/theories/sil/sil_sos.ml
+46 -46 metaprl/theories/sil/sil_sos.ml.new
+36 -36 metaprl/theories/sil/sil_state_model.ml
+23 -23 metaprl/theories/sil/sil_state_type.ml
+61 -61 metaprl/theories/sil/state_types.ml
+60 -60 metaprl/theories/tptp/tptp.ml
+73 -69 metaprl/theories/tptp/tptp.prla
+3 -3 metaprl/theories/tptp/tptp_prove.ml