Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] thms with VERY long identifiers

Email Gateway (Aug 18 2022 at 19:19):

From: Walther Neuper <wneuper@ist.tugraz.at>
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 ...

Last updated: Apr 30 2024 at 01:06 UTC