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;