src/CCL/Gfp.thy
author wenzelm
Sat, 17 Sep 2005 17:35:26 +0200
changeset 17456 bcf7544875b2
parent 1474 3f7d67927fe2
child 20140 98acc6d0fab6
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     1
(*  Title:      CCL/Gfp.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     7
header {* Greatest fixed points *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     8
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
     9
theory Gfp
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    10
imports Lfp
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    11
begin
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    12
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    13
constdefs
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    14
  gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    15
  "gfp(f) == Union({u. u <= f(u)})"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    16
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    17
ML {* use_legacy_bindings (the_context ()) *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 1474
diff changeset
    18
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
end