[isabelle-dev] simplification theorems generated for records:

Mamoun FILALI-AMINE filali at irit.fr
Thu Jul 28 16:17:18 CEST 2011


   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

record ('st,'act) ms =
   i :: "'st"

thm "ms.simps"

record ('st,'act) aut =
   m0 :: "'st"

thm "ms.simps"

(I use  (Isabelle2011: January 2011))


Mamoun Filali

-------------- next part --------------
A non-text attachment was scrubbed...
Name: filali.vcf
Type: text/x-vcard
Size: 277 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110728/8e0c7cbe/attachment.vcf>

More information about the isabelle-dev mailing list