diff -r 0418e9bffbba -r 585c3f2622ea src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri Apr 17 14:29:54 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Apr 17 14:29:55 2009 +0200
@@ -1,7 +1,6 @@
-(*  Authors:    Klaus Aehlig, Tobias Nipkow
-*)
+(*  Authors:  Klaus Aehlig, Tobias Nipkow *)
 
-header {* Test of normalization function *}
+header {* Testing implementation of normalization by evaluation *}
 
 theory NormalForm
 imports Main Rational
@@ -19,18 +18,13 @@
 
 datatype n = Z | S n
 
-consts
-  add :: "n \<Rightarrow> n \<Rightarrow> n"
-  add2 :: "n \<Rightarrow> n \<Rightarrow> n"
-  mul :: "n \<Rightarrow> n \<Rightarrow> n"
-  mul2 :: "n \<Rightarrow> n \<Rightarrow> n"
-  exp :: "n \<Rightarrow> n \<Rightarrow> n"
-primrec
-  "add Z = id"
-  "add (S m) = S o add m"
-primrec
-  "add2 Z n = n"
-  "add2 (S m) n = S(add2 m n)"
+primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "add Z = id"
+ | "add (S m) = S o add m"
+
+primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "add2 Z n = n"
+ | "add2 (S m) n = S(add2 m n)"
 
 declare add2.simps [code]
 lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
@@ -44,15 +38,17 @@
 lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
 lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
 
-primrec
-  "mul Z = (%n. Z)"
-  "mul (S m) = (%n. add (mul m n) n)"
-primrec
-  "mul2 Z n = Z"
-  "mul2 (S m) n = add2 n (mul2 m n)"
-primrec
-  "exp m Z = S Z"
-  "exp m (S n) = mul (exp m n) m"
+primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "mul Z = (%n. Z)"
+ | "mul (S m) = (%n. add (mul m n) n)"
+
+primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "mul2 Z n = Z"
+ | "mul2 (S m) n = add2 n (mul2 m n)"
+
+primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "exp m Z = S Z"
+ | "exp m (S n) = mul (exp m n) m"
 
 lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
 lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization