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 <[email protected]>: > > 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
