Nat.ML

 	     Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq, 
 	     nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
 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();
 
 val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<m::nat)";