Re: [isabelle] Fw : Re: Question on hypothesis



On 17/12/10 13:43, Tobias Nipkow wrote:
> olfa mraihi schrieb:
>   
>> 0)thank you very much for your usefull answer
>> 1)what does it mean [| |]?
>> 2)what does it mean P?
>>     
> Please refer to the extensive Isabelle documentation. This mailing list
> is intended to discuss technical questions and not to give an
> introduction to the system to save you reading the basic material.
>
>   
Since I've just looked at the indexes of several likely choices among
the Isabelle documentation, and the nearest I found to an adequate
answer to question (1) was an a manual described as "old" and
"outdated", it seems reasonable to answer it here.

[| P ; Q |] ==> R is an abbreviation (at the level of the parser and
prettyprinter) for
P ==> (Q ==> R)

Jeremy






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