arith.ML
changeset 21 803ccc4a83bb
parent 0 7949f97df77a
child 29 9769afcc1c4e
--- 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;