Re: [isabelle] Knaster-Tarski Lemma

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_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.


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