[isabelle-dev] simplification theorems generated for records:

[Brian Huffman]

Your confusion stems from the fact that your theory file is also
called "ms". The "simps" rules generated by the "record" command are
qualified by both the theory name and the type name, so the full names
in your example are "ms.ms.simps" and "ms.aut.simps". Referring to
either of these by their full names works just fine.

When you use an incomplete qualified name like "ms.simps", Isabelle
resolves this as the most recently defined name that matches. So at
the end of your example, "ms.simps" is resolved to "ms.aut.simps".

- Brian

2011/7/28 Mamoun FILALI-AMINE <filali at irit.fr>:
>
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>