--- a/src/HOLCF/Fix.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fix.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/fix.thy
+(* Title: HOLCF/Fix.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -37,5 +37,15 @@
flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
+(* further useful class for HOLCF *)
+
+axclass chfin<pcpo
+
+ax_chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+
+axclass flat<pcpo
+
+ax_flat "! x y.x << y --> (x = UU) | (x=y)"
+
end