[isabelle-dev] thms with VERY long identifiers

[Walther Neuper]

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