Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-10 13:41:19 -0700 (Sun, 10 Sep 2000)
Revision: 3058
Log message:

      Last commit failed partway through...
      

Changes  Path
+3552 -455 metaprl/theories/czf/czf_itt_rel.prla
+59 -14 metaprl/theories/czf/czf_itt_sall.ml
+2978 -618 metaprl/theories/czf/czf_itt_sall.prla
+126 -50 metaprl/theories/czf/czf_itt_sep.ml
+8 -8 metaprl/theories/czf/czf_itt_sep.mli
+6629 -5613 metaprl/theories/czf/czf_itt_sep.prla
+158 -48 metaprl/theories/czf/czf_itt_set.ml
+1 -0 metaprl/theories/czf/czf_itt_set.mli
+9001 -2699 metaprl/theories/czf/czf_itt_set.prla
+3272 -4139 metaprl/theories/czf/czf_itt_set_ind.prla
+62 -14 metaprl/theories/czf/czf_itt_sexists.ml
+2996 -626 metaprl/theories/czf/czf_itt_sexists.prla
+59 -9 metaprl/theories/czf/czf_itt_singleton.ml
+0 -15 metaprl/theories/czf/czf_itt_singleton.mli
+3518 -662 metaprl/theories/czf/czf_itt_singleton.prla
Binary metaprl/theories/czf/czf_itt_small.prlb
+71 -9 metaprl/theories/czf/czf_itt_subset.ml
+2 -2 metaprl/theories/czf/czf_itt_subset.mli
+2998 -1059 metaprl/theories/czf/czf_itt_subset.prla
Added metaprl/theories/czf/czf_itt_theory.mlz
Properties metaprl/theories/czf/czf_itt_theory.mlz
Added metaprl/theories/czf/czf_itt_theory.prla
Properties metaprl/theories/czf/czf_itt_theory.prla
+505 -452 metaprl/theories/czf/czf_itt_true.prla
+169 -33 metaprl/theories/czf/czf_itt_union.ml
+13 -38 metaprl/theories/czf/czf_itt_union.mli
+10310 -2754 metaprl/theories/czf/czf_itt_union.prla
Properties metaprl/theories/itt
Added metaprl/theories/itt/.ispell_english
Properties metaprl/theories/itt/.ispell_english
+1 -1 metaprl/theories/itt/Makefile
+63 -15 metaprl/theories/itt/itt_atom.ml
+64 -13 metaprl/theories/itt/itt_bisect.ml
+3975 -1371 metaprl/theories/itt/itt_bisect.prla
+217 -34 metaprl/theories/itt/itt_bool.ml
+12933 -6719 metaprl/theories/itt/itt_bool.prla
+55 -10 metaprl/theories/itt/itt_bunion.ml
+3180 -606 metaprl/theories/itt/itt_bunion.prla
+1788 -1001 metaprl/theories/itt/itt_collection.prla
Added metaprl/theories/itt/itt_comment.ml
Properties metaprl/theories/itt/itt_comment.ml
Added metaprl/theories/itt/itt_comment.mli
Properties metaprl/theories/itt/itt_comment.mli
+77 -6 metaprl/theories/itt/itt_decidable.ml
+5390 -2764 metaprl/theories/itt/itt_decidable.prla
+362 -338 metaprl/theories/itt/itt_derive.prla
+90 -46 metaprl/theories/itt/itt_dfun.ml
+0 -2 metaprl/theories/itt/itt_dfun.mli
+4754 -1477 metaprl/theories/itt/itt_dfun.prla
+198 -54 metaprl/theories/itt/itt_dprod.ml
+0 -0 metaprl/theories/itt/itt_dprod.mli
+138 -23 metaprl/theories/itt/itt_equal.ml
+13932 -7859 metaprl/theories/itt/itt_equal.prla
+126 -21 metaprl/theories/itt/itt_esquash.ml
+5858 -1078 metaprl/theories/itt/itt_esquash.prla
+4995 -4945 metaprl/theories/itt/itt_fset.prla
+77 -46 metaprl/theories/itt/itt_fun.ml
+0 -6 metaprl/theories/itt/itt_fun.mli
+5678 -2638 metaprl/theories/itt/itt_fun.prla
+108 -40 metaprl/theories/itt/itt_int.ml
+120 -29 metaprl/theories/itt/itt_isect.ml
+6480 -1646 metaprl/theories/itt/itt_isect.prla
+107 -59 metaprl/theories/itt/itt_list.ml
+7440 -3315 metaprl/theories/itt/itt_list.prla
+206 -32 metaprl/theories/itt/itt_list2.ml
+7826 -2645 metaprl/theories/itt/itt_list2.prla
+361 -46 metaprl/theories/itt/itt_logic.ml
+28866 -19300 metaprl/theories/itt/itt_logic.prla
+109 -51 metaprl/theories/itt/itt_prec.ml
+64 -31 metaprl/theories/itt/itt_prod.ml
+3651 -968 metaprl/theories/itt/itt_prod.prla
+360 -332 metaprl/theories/itt/itt_prop_decide.prla
+178 -77 metaprl/theories/itt/itt_quotient.ml
+146 -50 metaprl/theories/itt/itt_rfun.ml
+10760 -4718 metaprl/theories/itt/itt_rfun.prla
+96 -31 metaprl/theories/itt/itt_set.ml
+2431 -1997 metaprl/theories/itt/itt_sort.prla
+88 -12 metaprl/theories/itt/itt_squash.ml
+1 -0 metaprl/theories/itt/itt_squash.mli
+89 -46 metaprl/theories/itt/itt_srec.ml
+229 -54 metaprl/theories/itt/itt_struct.ml
+10085 -3677 metaprl/theories/itt/itt_struct.prla
+98 -36 metaprl/theories/itt/itt_subtype.ml
+28 -10 metaprl/theories/itt/itt_theory.ml
+76 -9 metaprl/theories/itt/itt_tunion.ml
+105 -37 metaprl/theories/itt/itt_union.ml
+65 -27 metaprl/theories/itt/itt_unit.ml
+55 -25 metaprl/theories/itt/itt_void.ml
Added metaprl/theories/itt/itt_void.prla
Properties metaprl/theories/itt/itt_void.prla
+105 -38 metaprl/theories/itt/itt_w.ml
+59 -9 metaprl/theories/itt/itt_well_founded.ml
+3300 -387 metaprl/theories/itt/itt_well_founded.prla
+4 -2 metaprl/theories/ocaml/ocaml_expr_df.ml
Added metaprl/theories/tactic/.ispell_english
Properties metaprl/theories/tactic/.ispell_english
+6 -3 metaprl/theories/tactic/Makefile
Added metaprl/theories/tactic/base_dform.ml
Properties metaprl/theories/tactic/base_dform.ml
Added metaprl/theories/tactic/base_dform.mli
Properties metaprl/theories/tactic/base_dform.mli
Added metaprl/theories/tactic/comment.ml
Properties metaprl/theories/tactic/comment.ml
Added metaprl/theories/tactic/comment.mli
Properties metaprl/theories/tactic/comment.mli
+74 -5 metaprl/theories/tactic/mptop.ml
+1 -0 metaprl/theories/tactic/mptop.mli
+48 -13 metaprl/theories/tactic/nuprl_font.ml
+2 -0 metaprl/theories/tactic/nuprl_font.mli
+54 -7 metaprl/theories/tactic/perv.ml
Added metaprl/theories/tactic/summary.ml
Properties metaprl/theories/tactic/summary.ml
Added metaprl/theories/tactic/summary.mli
Properties metaprl/theories/tactic/summary.mli
+250 -18 metaprl/theories/tactic/top_conversionals.ml
+363 -39 metaprl/theories/tactic/top_tacticals.ml
+39 -3 metaprl/theories/tactic/var.ml