Re: [isabelle] [isabelle-dev] simplification theorems generated for records:



I am reposting my response to the Isabelle-users mailing list (from
the dev list) since that is the proper venue for this question...

On Thu, Jul 28, 2011 at 7:28 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> 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
>>
>>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.