changeset 1410 | 324aa8134639 |
parent 1168 | 74be52691d62 |
child 1479 | 21eb5e156d91 |
--- a/src/HOLCF/Fix.thy Mon Dec 18 13:09:17 1995 +0100 +++ b/src/HOLCF/Fix.thy Wed Dec 20 16:28:51 1995 +0100 @@ -18,7 +18,7 @@ adm :: "('a=>bool)=>bool" admw :: "('a=>bool)=>bool" chain_finite :: "'a=>bool" -flat :: "'a=>bool" +is_flat :: "'a=>bool" defs @@ -35,7 +35,7 @@ chain_finite_def "chain_finite (x::'a)== !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)" -flat_def "flat (x::'a) == +is_flat_def "is_flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)" end