# HG changeset patch
# User berghofe
# Date 832933624 -7200
# Node ID 0c8f131eac408d6f04f036e1c1a9125e96dba619
# Parent  23922221ac875ead3de4fe354597641e85222bc9
Rules pred_0, pred_Suc etc. are now stored in theorem database.

diff -r 23922221ac87 -r 0c8f131eac40 src/HOL/Arith.ML
--- 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 **)