1.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Sep 12 14:59:44 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Sep 12 15:43:15 2000 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  Let us look at an example:
     1.5  *}
     1.6  
     1.7 -consts gcd :: "nat*nat \\<Rightarrow> nat";
     1.8 +consts gcd :: "nat\<times>nat \\<Rightarrow> nat";
     1.9  recdef gcd "measure (\\<lambda>(m,n).n)"
    1.10    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
    1.11  
    1.12 @@ -48,7 +48,7 @@
    1.13  following alternative definition suggests itself:
    1.14  *}
    1.15  
    1.16 -consts gcd1 :: "nat*nat \\<Rightarrow> nat";
    1.17 +consts gcd1 :: "nat\<times>nat \\<Rightarrow> nat";
    1.18  recdef gcd1 "measure (\\<lambda>(m,n).n)"
    1.19    "gcd1 (m, 0) = m"
    1.20    "gcd1 (m, n) = gcd1(n, m mod n)";
    1.21 @@ -63,7 +63,7 @@
    1.22  is also available for @{typ"bool"} but is not split automatically:
    1.23  *}
    1.24  
    1.25 -consts gcd2 :: "nat*nat \\<Rightarrow> nat";
    1.26 +consts gcd2 :: "nat\<times>nat \\<Rightarrow> nat";
    1.27  recdef gcd2 "measure (\\<lambda>(m,n).n)"
    1.28    "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
    1.29  
    1.30 @@ -83,7 +83,7 @@
    1.31  after which we can disable the original simplification rule:
    1.32  *}
    1.33  
    1.34 -lemmas [simp del] = gcd.simps;
    1.35 +declare gcd.simps [simp del]
    1.36  
    1.37  (*<*)
    1.38  end