--- a/src/HOLCF/Fix.thy Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Fix.thy Sun May 25 16:17:09 1997 +0200
@@ -17,8 +17,6 @@
fix :: "('a->'a)->'a"
adm :: "('a::cpo=>bool)=>bool"
admw :: "('a=>bool)=>bool"
-chain_finite :: "'a::cpo=>bool"
-flat :: "'a=>bool"
defs
@@ -32,16 +30,11 @@
admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
P (lub(range (%i. iterate i F UU)))"
-chain_finite_def "chain_finite (x::'a::cpo)==
- !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)"
-
-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)"
+chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
axclass flat<pcpo