src/HOLCF/Lift.thy
 changeset 12338 de0f4a63baa5 parent 12026 0b1d80ada4ab child 14096 f79d139c7e46
```     1.1 --- a/src/HOLCF/Lift.thy	Sat Dec 01 18:51:46 2001 +0100
1.2 +++ b/src/HOLCF/Lift.thy	Sat Dec 01 18:52:32 2001 +0100
1.3 @@ -4,11 +4,11 @@
1.5  *)
1.6
1.7 -header {* Lifting types of class term to flat pcpo's *}
1.8 +header {* Lifting types of class type to flat pcpo's *}
1.9
1.10  theory Lift = Cprod3:
1.11
1.12 -defaultsort "term"
1.13 +defaultsort type
1.14
1.15
1.16  typedef 'a lift = "UNIV :: 'a option set" ..
1.17 @@ -19,12 +19,12 @@
1.18    Def :: "'a => 'a lift"
1.19    "Def x == Abs_lift (Some x)"
1.20
1.21 -instance lift :: ("term") sq_ord ..
1.22 +instance lift :: (type) sq_ord ..
1.23
1.25    less_lift_def: "x << y == (x=y | x=Undef)"
1.26
1.27 -instance lift :: ("term") po
1.28 +instance lift :: (type) po
1.29  proof
1.30    fix x y z :: "'a lift"
1.31    show "x << x" by (unfold less_lift_def) blast
1.32 @@ -111,7 +111,7 @@
1.33    apply (blast intro: lub_finch1)
1.34    done
1.35
1.36 -instance lift :: ("term") pcpo
1.37 +instance lift :: (type) pcpo
1.38    apply intro_classes
1.39     apply (erule cpo_lift)
1.40    apply (rule least_lift)
1.41 @@ -153,7 +153,7 @@
1.42  consts
1.43   flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
1.44   flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
1.45 - liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
1.46 + liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
1.47
1.48  defs
1.49   flift1_def:
1.50 @@ -219,7 +219,7 @@
1.51
1.52  subsection {* Lift is flat *}
1.53
1.54 -instance lift :: ("term") flat
1.55 +instance lift :: (type) flat
1.56  proof
1.57    show "ALL x y::'a lift. x << y --> x = UU | x = y"