changeset 40431 | 682d6c455670 |
parent 40002 | c5b5f7a3a3b1 |
--- a/src/HOLCF/ex/Fix2.thy Wed Nov 03 15:31:24 2010 -0700 +++ b/src/HOLCF/ex/Fix2.thy Wed Nov 03 15:47:46 2010 -0700 @@ -17,7 +17,7 @@ lemma lemma1: "fix = gix" apply (rule cfun_eqI) -apply (rule antisym_less) +apply (rule below_antisym) apply (rule fix_least) apply (rule gix1_def) apply (rule gix2_def)