Email Gateway (Aug 18 2022 at 12:28): Email Gateway (Aug 18 2022 at 12:28):From: David Trachtenherz <trachten@in.tum.de>
Hello,
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?
Thank You in advance!
David
Email Gateway (Aug 18 2022 at 12:28):From: Makarius <makarius@sketis.net>
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
Last updated: Nov 21 2024 at 12:39 UTC