Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lfp.thy
author nipkow
Tue, 09 May 1995 22:10:08 +0200
changeset 1114 c8dfb56a7e95
parent 923 ff1574a81019
child 1264 3eb91524b938
permissions -rw-r--r--
Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     1
 
(*  Title: 	HOL/lfp.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     2
 
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     3
 
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     4
 
    Copyright   1992  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     5
 












ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




     6


The Knaster-Tarski Theorem













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




     7


*)













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




     8









1114






c8dfb56a7e95
Prod is now a parent of Lfp.



nipkow


parents: 
923

diff
changeset




     9


Lfp = mono + Prod +








923






ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    10


consts lfp :: "['a set=>'a set] => 'a set"













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    11


defs













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    12


 (*least fixed point*)













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    13


 lfp_def "lfp(f) == Inter({u. f(u) <= u})"













ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    14


end















isabelle