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 sketis.net> wrote:
> On Sat, 30 Nov 2013, Alfio Martini wrote:
> However, even after importing Lattice_Syntax it is still necessary to
>> provide the following
>> 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_
> 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.
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