Re: [isabelle] [isabelle-dev] thms with VERY long identifiers



It seems that the numeric indexing works if you omit the double quotes:

@{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)}

On Mon, Mar 19, 2012 at 3:32 PM, Walther Neuper <wneuper at ist.tugraz.at> wrote:
> 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
>     at {thm "NthRoot.four_x_squared"};
> which works, but
>     at {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
> 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.