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 oheimb
Sat, 15 Feb 1997 17:48:19 +0100
changeset 2636 4b30dbe4a020
parent 1558 9c6ebfab4e05
child 3947 eb707467f8c5
permissions -rw-r--r--
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1370
diff changeset 
     1
 
(*  Title:      HOL/Lfp.thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset 
     2
 
    ID:         $Id$
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1370
diff changeset 
     3
 
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
923
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 +








1558






9c6ebfab4e05
added constdefs section



clasohm


parents: 
1475

diff
changeset




    10














9c6ebfab4e05
added constdefs section



clasohm


parents: 
1475

diff
changeset




    11


constdefs













9c6ebfab4e05
added constdefs section



clasohm


parents: 
1475

diff
changeset




    12


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













9c6ebfab4e05
added constdefs section



clasohm


parents: 
1475

diff
changeset




    13


  "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)













9c6ebfab4e05
added constdefs section



clasohm


parents: 
1475

diff
changeset




    14









923






ff1574a81019
new version of HOL with curried function application



clasohm


parents: 

diff
changeset




    15


end















isabelle