--- a/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Tue Sep 12 15:43:15 2000 +0200
@@ -11,7 +11,7 @@
Let us look at an example:
*}
-consts gcd :: "nat*nat \\<Rightarrow> nat";
+consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd "measure (\\<lambda>(m,n).n)"
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
@@ -48,7 +48,7 @@
following alternative definition suggests itself:
*}
-consts gcd1 :: "nat*nat \\<Rightarrow> nat";
+consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd1 "measure (\\<lambda>(m,n).n)"
"gcd1 (m, 0) = m"
"gcd1 (m, n) = gcd1(n, m mod n)";
@@ -63,7 +63,7 @@
is also available for @{typ"bool"} but is not split automatically:
*}
-consts gcd2 :: "nat*nat \\<Rightarrow> nat";
+consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
recdef gcd2 "measure (\\<lambda>(m,n).n)"
"gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
@@ -83,7 +83,7 @@
after which we can disable the original simplification rule:
*}
-lemmas [simp del] = gcd.simps;
+declare gcd.simps [simp del]
(*<*)
end