[isabelle] thms with VERY long identifiers



by find_theorems searching for
   "_ * _ = _ ^ _"
    found 6 theorem(s) in 0.120 secs:
    NthRoot.four_x_squared: 4 * ?x\<twosuperior> = (2 * ?x)\<twosuperior>
    :
Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29):
      ?x * ?x = ?x\<twosuperior>

I try
    @{thm "NthRoot.four_x_squared"};
which works, but
@{thm "Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)"};
does not work.

Is there a direct way to create an individual identifier "xxx" for this theorem, which can be used in @{thm "xxx"} ?

I am searching the documentation for some while ---
--- but probably there is someone with a quick hint ?

Walther


PS: sorry for that ...

On 03/19/2012 04:07 PM, Makarius wrote:
On Mon, 19 Mar 2012, Walther Neuper wrote:

I am searching the documentation for some while --- --- but probably there is someone with a quick hint ?

There seems to be an identity crisis of the isabelle-users mailing list, since regular user questions are asked in this narrow forum that mainly addresses the Isabelle development process.


    Makarius






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