| changeset 13524 | 604d0f3622d6 |
| parent 10835 | f4745d77e620 |
| child 16218 | ea49a9c7ff7c |
--- a/src/HOLCF/ex/loeckx.ML Tue Aug 27 11:03:02 2002 +0200 +++ b/src/HOLCF/ex/loeckx.ML Tue Aug 27 11:03:05 2002 +0200 @@ -66,7 +66,7 @@ by (rtac cont2cont_CF1L 1); by (rtac cont_iterate 1); by (rtac (chain_iterate RS chainE) 1); -qed "cont_Ifix2"; +qed "cont_Ifix2'"; (* the proof in little steps *) @@ -98,5 +98,5 @@ by (rtac cont2cont_CF1L 1); by (rtac cont_iterate 1); by (rtac (chain_iterate RS chainE) 1); -qed "cont_Ifix2"; +qed "cont_Ifix2''";