1993-09-20 lcp [Mon, 20 Sep 1993 18:39:45 +0200] rev 9
make-all now has set +e so that New Jersey runs will continue even if some
logic fails. change_simp added to help change to new simplifier.
change_simp make-all src/Tools/change_simp src/Tools/make-all

1993-09-20 lcp [Mon, 20 Sep 1993 17:02:11 +0200] rev 8
Installation of new simplfier. Previously appeared to set up the old
simplifier to rewrite with the partial ordering [=, something not possible
with the new simplifier. But such rewriting appears not to have actually
been used, and there were few complications. In terms.ML setloop was used
to avoid infinite rewriting with the letrec rule. Congruence rules were
deleted, and an occasional SIMP_TAC had to become asm_simp_tac.
src/CCL/CCL.ML src/CCL/Fix.ML src/CCL/Hered.ML src/CCL/Set.ML src/CCL/Term.ML src/CCL/Type.ML src/CCL/Wfd.ML src/CCL/ccl.ML src/CCL/coinduction.ML src/CCL/ex/List.ML src/CCL/ex/Nat.ML src/CCL/ex/Stream.ML src/CCL/ex/list.ML src/CCL/ex/nat.ML src/CCL/ex/stream.ML src/CCL/fix.ML src/CCL/hered.ML src/CCL/set.ML src/CCL/subset.ML src/CCL/term.ML src/CCL/terms.ML src/CCL/type.ML src/CCL/wfd.ML

1993-09-17 lcp [Fri, 17 Sep 1993 16:52:10 +0200] rev 7
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
particularly delicate. There is a variable renaming problem in
ramsey.ML/pigeon2_lemma. In some cases, rewriting by typechecking rules
had to be replaced by setsolver type_auto_tac... because only the solver
can instantiate variables.
src/ZF/ex/BT_Fn.ML src/ZF/ex/BinFn.ML src/ZF/ex/Enum.ML src/ZF/ex/Equiv.ML src/ZF/ex/Integ.ML src/ZF/ex/LList.ML src/ZF/ex/ListN.ML src/ZF/ex/PropLog.ML src/ZF/ex/Ramsey.ML src/ZF/ex/TF_Fn.ML src/ZF/ex/TermFn.ML src/ZF/ex/binfn.ML src/ZF/ex/bt_fn.ML src/ZF/ex/enum.ML src/ZF/ex/equiv.ML src/ZF/ex/integ.ML src/ZF/ex/listn.ML src/ZF/ex/llist.ML src/ZF/ex/misc.ML src/ZF/ex/proplog.ML src/ZF/ex/ramsey.ML src/ZF/ex/termfn.ML src/ZF/ex/tf_fn.ML

1993-09-17 lcp [Fri, 17 Sep 1993 16:16:38 +0200] rev 6
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
src/ZF/Arith.ML src/ZF/Arith.thy src/ZF/Bool.ML src/ZF/Epsilon.ML src/ZF/List.ML src/ZF/ListFn.ML src/ZF/Nat.ML src/ZF/Nat.thy src/ZF/Ord.ML src/ZF/Pair.ML src/ZF/Perm.ML src/ZF/QPair.ML src/ZF/QUniv.ML src/ZF/ROOT.ML src/ZF/Sum.ML src/ZF/Univ.ML src/ZF/WF.ML src/ZF/ZF.ML src/ZF/arith.ML src/ZF/arith.thy src/ZF/bool.ML src/ZF/constructor.ML src/ZF/epsilon.ML src/ZF/fin.ML src/ZF/func.ML src/ZF/ind-syntax.ML src/ZF/ind_syntax.ML src/ZF/list.ML src/ZF/listfn.ML src/ZF/nat.ML src/ZF/nat.thy src/ZF/ord.ML src/ZF/pair.ML src/ZF/perm.ML src/ZF/qpair.ML src/ZF/quniv.ML src/ZF/simpdata.ML src/ZF/sum.ML src/ZF/univ.ML src/ZF/upair.ML src/ZF/wf.ML src/ZF/zf.ML

1993-09-17 lcp [Fri, 17 Sep 1993 12:53:53 +0200] rev 5
test commit
src/ZF/ROOT.ML

1993-09-16 nipkow [Thu, 16 Sep 1993 17:41:10 +0200] rev 4
added header
src/Provers/splitter.ML

1993-09-16 nipkow [Thu, 16 Sep 1993 16:55:17 +0200] rev 3
defined local addcongs
src/FOL/simpdata.ML

1993-09-16 clasohm [Thu, 16 Sep 1993 16:25:32 +0200] rev 2
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
src/Pure/ROOT.ML

1993-09-16 nipkow [Thu, 16 Sep 1993 14:21:44 +0200] rev 1
changed addcongs to addeqcongs in simplifier.ML
src/Provers/simp.ML src/Provers/simplifier.ML

1993-09-16 clasohm [Thu, 16 Sep 1993 12:20:38 +0200] rev 0
Initial revision
CHANGES-92f.txt COPYRIGHT EMAILDIST-README README agrep edits.txt expandshort get-rulenames make-all make-dist make-rulenames prove_goal.el rm-logfiles src/CCL/CCL.ML src/CCL/CCL.thy src/CCL/Fix.ML src/CCL/Fix.thy src/CCL/Gfp.ML src/CCL/Gfp.thy src/CCL/Hered.ML src/CCL/Hered.thy src/CCL/Lfp.ML src/CCL/Lfp.thy src/CCL/Makefile src/CCL/ROOT.ML src/CCL/Set.ML src/CCL/Set.thy src/CCL/Term.ML src/CCL/Term.thy src/CCL/Trancl.ML src/CCL/Trancl.thy src/CCL/Type.ML src/CCL/Type.thy src/CCL/Wfd.ML src/CCL/Wfd.thy src/CCL/ccl.ML src/CCL/ccl.thy src/CCL/coinduction.ML src/CCL/equalities.ML src/CCL/eval.ML src/CCL/ex/Flag.ML src/CCL/ex/Flag.thy src/CCL/ex/List.ML src/CCL/ex/List.thy src/CCL/ex/Nat.ML src/CCL/ex/Nat.thy src/CCL/ex/ROOT.ML src/CCL/ex/Stream.ML src/CCL/ex/Stream.thy src/CCL/ex/flag.ML ...