Mon, 20 Sep 1993 17:02:11 +0200 Installation of new simplfier. Previously appeared to set up the old
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.
Fri, 17 Sep 1993 16:52:10 +0200 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
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.
Fri, 17 Sep 1993 16:16:38 +0200 Installation of new simplifier for ZF. Deleted all congruence rules not
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.
(0) -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip