[isabelle-dev] simplification theorems generated for records:

[Mamoun FILALI-AMINE]

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


-------------- 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>