# HG changeset patch # User paulson # Date 864642818 -7200 # Node ID 29ddef80bd4924422af239a1e29d962d37cb690b # Parent b0139b83a5eef073ba84e095d53cfc4361304eb6 Renamed lessD to Suc_leI diff -r b0139b83a5ee -r 29ddef80bd49 src/HOL/ex/Puzzle.ML --- a/src/HOL/ex/Puzzle.ML Mon May 26 12:33:03 1997 +0200 +++ b/src/HOL/ex/Puzzle.ML Mon May 26 12:33:38 1997 +0200 @@ -22,7 +22,7 @@ by (dtac not_leE 1); by (subgoal_tac "f(na) <= f(f(na))" 1); by (fast_tac (!claset addIs [Puzzle.f_ax]) 2); -by (rtac lessD 1); +by (rtac Suc_leI 1); by (fast_tac (!claset delrules [order_refl] addIs [Puzzle.f_ax, le_less_trans]) 1); val lemma = result() RS spec RS mp; @@ -56,5 +56,5 @@ goal Puzzle.thy "f(n) = n"; by (rtac le_anti_sym 1); by (rtac lemma1 2); -by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1); +by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,Suc_leI]) 1); result();