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