diff -r 2c38796b33b9 -r ee4dfce170a0 src/HOLCF/Fix.thy
--- 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