| changeset 6676 | 62d1e642da30 |
| parent 5618 | 721671c68324 |
| child 8018 | bedd0beabbae |
--- a/src/HOL/ex/Puzzle.ML Fri May 21 10:50:04 1999 +0200 +++ b/src/HOL/ex/Puzzle.ML Fri May 21 10:56:46 1999 +0200 @@ -55,7 +55,7 @@ qed "f_mono"; Goal "f(n) = n"; -by (rtac le_anti_sym 1); +by (rtac order_antisym 1); by (rtac lemma1 2); by (fast_tac (claset() addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); result();