isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Fri, 17 Sep 1993 16:52:10 +0200 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is

changeset

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

changeset

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.

Fri, 17 Sep 1993 12:53:53 +0200 test commit

changeset

lcp [Fri, 17 Sep 1993 12:53:53 +0200] rev 5

test commit

Thu, 16 Sep 1993 17:41:10 +0200 added header

changeset

nipkow [Thu, 16 Sep 1993 17:41:10 +0200] rev 4

added header

Thu, 16 Sep 1993 16:55:17 +0200 defined local addcongs

changeset

nipkow [Thu, 16 Sep 1993 16:55:17 +0200] rev 3

defined local addcongs