Re: [isabelle] Knaster-Tarski Lemma

Thanks Makarius.  If only I had remembered to take a look at this folder
from the start, I would have
saved myself a couple of hours (to put it mildly)...


On Sun, Dec 1, 2013 at 1:24 PM, Makarius <makarius at> wrote:

> On Sat, 30 Nov 2013, Alfio Martini wrote:
>  However, even after importing Lattice_Syntax it is still necessary to
>> provide the following
>> declaration
>> notation
>>  less_eq (infix "⊑" 50)
>> Its is hidden (via no_notation) at the end of Complete_Lattice and not
>> available in Lattice_Syntax.thy
> A fully authentic version of the example is $ISABELLE_HOME/src/HOL/Isar_
> Examples/Knaster_Tarski.thy
> The "printed" versions in papers and slides that appeared over the years
> occasionally vary in some requirements of notation, or even some implicit
> rule declarations for lattice theory.
> Note that this example was the first non-trivial Isar proof in history.
> The Isar proof before it was for "A --> A", the one after it the
> Hahn-Banach Theorem formalized by Gertrud Bauer on 40 pages.
>         Makarius

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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