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

I beg to disagree. The Tutorial (not under old/outdated) has "[|" and
"|]" in the index, pointing to a table that explains that they are the
same as the similar looking symbols [| |], and those symbols are used
throughout the documentation, in particular on page 13, where it is
explained that they group together assumptions. I consider this an
adequate explanation.


Jeremy Dawson schrieb:
> 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.