Rules pred_0, pred_Suc etc. are now stored in theorem database.

--- a/src/HOL/Arith.ML	Fri May 24 11:48:18 1996 +0200
+++ b/src/HOL/Arith.ML	Fri May 24 12:27:04 1996 +0200
@@ -13,7 +13,13 @@
 
 val [pred_0, pred_Suc] = nat_recs pred_def;
 val [add_0,add_Suc] = nat_recs add_def; 
-val [mult_0,mult_Suc] = nat_recs mult_def; 
+val [mult_0,mult_Suc] = nat_recs mult_def;
+store_thm("pred_0",pred_0);
+store_thm("pred_Suc",pred_Suc);
+store_thm("add_0",add_0);
+store_thm("add_Suc",add_Suc);
+store_thm("mult_0",mult_0);
+store_thm("mult_Suc",mult_Suc);
 Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
 
 (** pred **)