# HG changeset patch
# User paulson
# Date 904637411 -7200
# Node ID 5ed7547a7f742c639f0b93de33e0b91f7b25c796
# Parent  e97558ee8e76c00b5dc406e5ee1da9d13fceef37
Moved lemmas to Arith.ML

diff -r e97558ee8e76 -r 5ed7547a7f74 src/HOL/UNITY/Lift.ML
--- 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";