--- 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;
--- a/Arith.thy Mon Nov 29 18:35:02 1993 +0100
+++ b/Arith.thy Tue Nov 30 17:44:04 1993 +0100
@@ -11,8 +11,10 @@
nat::minus
nat::times
consts
+ pred :: "nat => nat"
div,mod :: "[nat,nat]=>nat" (infixl 70)
rules
+ pred_def "pred(m) == nat_rec(m, 0, %n r.n)"
add_def "m+n == nat_rec(m, n, %u v.Suc(v))"
diff_def "m-n == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))"
mult_def "m*n == nat_rec(m, 0, %u v. n + v)"
--- 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;
--- a/arith.thy Mon Nov 29 18:35:02 1993 +0100
+++ b/arith.thy Tue Nov 30 17:44:04 1993 +0100
@@ -11,8 +11,10 @@
nat::minus
nat::times
consts
+ pred :: "nat => nat"
div,mod :: "[nat,nat]=>nat" (infixl 70)
rules
+ pred_def "pred(m) == nat_rec(m, 0, %n r.n)"
add_def "m+n == nat_rec(m, n, %u v.Suc(v))"
diff_def "m-n == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))"
mult_def "m*n == nat_rec(m, 0, %u v. n + v)"