Re: [isabelle] Adding lemmas to fact collections



On Sat, 27 Sep 2008, David Trachtenherz wrote:

> in Isabelle 2005 it was possible to successively add lemmas to a
> collection of lemmas in a way like:
> lemmas some_lemmas = lemma1 lemma2
> lemmas some_lemmas = some_lemmas lemma3
> lemmas some_lemmas = some_lemmas lemma4
> ...
> 
> In Isabelle 2008 this method yields the error message "Duplicate fact".
> Is there a way to add new facts to an already declared fact collection?

Overwriting existing fact names in older versions of Isabelle did not 
really achieve the effect of "adding facts to a collection", and had many 
other problems (there was also a warning).  For example, merging theories 
did not merge these pseudo-containers, but select one from some branch 
(via the name space).

This is how to do named collections of facts properly in Isabelle2008:

ML {* structure Foo = NamedThmsFun(val name = "foo" val description = "foo rules") *}
setup Foo.setup

declare refl [foo]
declare sym [foo]
declare trans [foo]

thm foo

declare refl [foo del]

thm foo


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.