src/HOL/UNITY/Lift.ML
changeset 5410 5ed7547a7f74
parent 5357 6efb2b87610c
child 5424 771a68a468cc
--- a/src/HOL/UNITY/Lift.ML	Tue Sep 01 10:09:11 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Tue Sep 01 10:10:11 1998 +0200
@@ -61,16 +61,6 @@
 val nat_exhaust_pred_le = 
     read_instantiate_sg (sign_of thy) [("P", "?y-1 <= ?m")] nat.exhaust;
 
-Goal "0 < n ==> (m <= n-1) = (m<n)";
-by (exhaust_tac "n" 1);
-by Auto_tac;
-qed "le_pred_eq";
-
-Goal "0 < n ==> (m-1 < n) = (m<=n)";
-by (exhaust_tac "m" 1);
-by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
-qed "less_pred_eq";
-
 Goal "m < n ==> m <= n-1";
 by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
 qed "less_imp_le_pred";