--- a/Nat.ML Thu Sep 16 14:29:14 1993 +0200
+++ b/Nat.ML Wed Sep 22 15:43:05 1993 +0200
@@ -351,6 +351,15 @@
val nat_ss = pair_ss addsimps nat_simps;
+(*Prevents simplification of f and g: much faster*)
+val nat_case_weak_cong = prove_goal Nat.thy
+ "m=n ==> nat_case(m,a,f) = nat_case(n,a,f)"
+ (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+val nat_rec_weak_cong = prove_goal Nat.thy
+ "m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
+ (fn [prem] => [rtac (prem RS arg_cong) 1]);
+
val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=n::nat";
by (resolve_tac prems 1);
val leI = result();