--- a/src/HOLCF/Pcpo.thy Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Pcpo.thy Thu Oct 06 18:40:18 1994 +0100
@@ -1,38 +1,14 @@
-(* Title: HOLCF/pcpo.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Definition of class pcpo (pointed complete partial order)
-
-The prototype theory for this class is porder.thy
-
-*)
-
Pcpo = Porder +
-(* Introduction of new class. The witness is type void. *)
-
classes pcpo < po
-
-(* default class is still term *)
-(* void is the prototype in pcpo *)
-
arities void :: pcpo
consts
- UU :: "'a::pcpo" (* UU is the least element *)
+ UU :: "'a::pcpo"
rules
-(* class axioms: justification is theory Porder *)
-
-minimal "UU << x" (* witness is minimal_void *)
-
-cpo "is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))"
- (* witness is cpo_void *)
- (* needs explicit type *)
-
-(* instance of UU for the prototype void *)
+minimal "UU << x"
+cpo "is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)"
inst_void_pcpo "(UU::void) = UU_void"