diff -r f4f9946ad741 -r 803ccc4a83bb Arith.ML
--- a/Arith.ML	Mon Nov 29 18:35:02 1993 +0100
+++ b/Arith.ML	Tue Nov 30 17:44:04 1993 +0100
@@ -11,8 +11,9 @@
 
 open Arith;
 
-(*** Basic rewrite and congruence rules for the arithmetic operators ***)
+(*** Basic rewrite rules for the arithmetic operators ***)
 
+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;