diff -r fa4aebe5b6f1 -r da0e86b4b352 IOA/example/Lemmas.ML
--- a/IOA/example/Lemmas.ML	Wed Mar 01 17:37:09 1995 +0100
+++ b/IOA/example/Lemmas.ML	Wed Mar 01 17:44:05 1995 +0100
@@ -126,11 +126,6 @@
  by (assume_tac 1);
 qed "less_add_cong";
 
-goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
-  by (dtac le_imp_less_or_eq 1);
-  by (fast_tac (HOL_cs addIs [less_trans]) 1);
-qed "less_leq_less";
-
 goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D";
   by (rtac impI 1);
   by (rtac impI 1);
@@ -211,23 +206,12 @@
   by (asm_simp_tac arith_ss 1);
 qed "unzero_less";
 
-(* Duplicate of earlier lemma! *)
-goal Arith.thy "x<(y::nat) --> y<=z --> x<(z::nat)";
-  by (rtac impI 1); by (rtac impI 1);
-  by (dtac  le_imp_less_or_eq 1);
-  by (fast_tac (HOL_cs addIs [less_trans]) 1);
-qed "less_leq_less";
-
-goal Arith.thy "(Suc(n) <= Suc(m)) = (n <= m)";
-  by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1);
-qed "succ_leq_mono";
-
 (* Odd proof. Why do induction? *)
 goal Arith.thy "((x::nat) = y + z) --> (y <= x)";
   by (nat_ind_tac "y" 1);
   by (simp_tac arith_ss 1);
   by (simp_tac (arith_ss addsimps 
-                [succ_leq_mono, le_refl RS (leq_add_leq RS mp)]) 1);
+                [Suc_le_mono, le_refl RS (leq_add_leq RS mp)]) 1);
 qed "plus_leq_lem";
 
 (* Lists *)