Hello,
The simplification theorems generated for records
seems to be overwritten: in the following text,
the first thm "ms.simps" prints the correct list
while the second thm "ms.simps" prints the list for the
preceding record.
theory ms imports Main
begin
record ('st,'act) ms =
i :: "'st"
thm "ms.simps"
record ('st,'act) aut =
m0 :: "'st"
thm "ms.simps"
(I use (Isabelle2011: January 2011))
thanks
Mamoun Filali
<<attachment: filali.vcf>>
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
