# HG changeset patch
# User wenzelm
# Date 1002544142 -7200
# Node ID ecdfd237ffee8a1ad94f5de8b2a94cee9811a661
# Parent  f5401162c9f00b245e66a567faa39df1a659dfd6
fixed numerals;

diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -78,9 +78,9 @@
 
 consts integer_arity :: "integer_op \<Rightarrow> nat"
 primrec
-"integer_arity (Number n)        = #0"
-"integer_arity UnaryMinus        = #1"
-"integer_arity Plus              = #2"
+"integer_arity (Number n)        = 0"
+"integer_arity UnaryMinus        = 1"
+"integer_arity Plus              = 2"
 
 consts well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
 inductive "well_formed_gterm arity"
diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -66,7 +66,7 @@
 simple arithmetic goals automatically:
 *}
 
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+lemma "\<lbrakk> \<not> m < n; m < n + (1::nat) \<rbrakk> \<Longrightarrow> m = n"
 (*<*)by(auto)(*>*)
 
 text{*\noindent
@@ -75,7 +75,7 @@
 In consequence, @{text auto} cannot prove this slightly more complex goal:
 *}
 
-lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
+lemma "\<not> m < n \<and> m < n + (1::nat) \<Longrightarrow> m = n";
 (*<*)by(arith)(*>*)
 
 text{*\noindent
diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -21,12 +21,12 @@
 apply (simp add: is_gcd)
 done
 
-lemma gcd_1 [simp]: "gcd(m,1') = 1'"
+lemma gcd_1 [simp]: "gcd(m, Suc 0) = Suc 0"
 apply simp
 done
 
-lemma gcd_1_left [simp]: "gcd(1',m) = 1'"
-apply (simp add: gcd_commute [of "1'"])
+lemma gcd_1_left [simp]: "gcd(Suc 0, m) = Suc 0"
+apply (simp add: gcd_commute [of "Suc 0"])
 done
 
 text{*\noindent
@@ -125,7 +125,7 @@
 \rulename{arg_cong}
 *}
 
-lemma "#2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
+lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
 apply intro
 txt{*
 before using arg_cong
@@ -177,7 +177,7 @@
 by (blast intro: relprime_dvd_mult dvd_trans)
 
 
-lemma relprime_20_81: "gcd(#20,#81) = 1";
+lemma relprime_20_81: "gcd(20,81) = 1";
 by (simp add: gcd.simps)
 
 text {*
@@ -199,14 +199,14 @@
 @{thm[display] dvd_add [OF _ dvd_refl]}
 *};
 
-lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)";
-apply (subgoal_tac "z = #34 \<or> z = #36")
+lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
+apply (subgoal_tac "z = 34 \<or> z = 36")
 txt{*
 the tactic leaves two subgoals:
 @{subgoals[display,indent=0,margin=65]}
 *};
 apply blast
-apply (subgoal_tac "z \<noteq> #35")
+apply (subgoal_tac "z \<noteq> 35")
 txt{*
 the tactic leaves two subgoals:
 @{subgoals[display,indent=0,margin=65]}
diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -12,7 +12,7 @@
 by (drule mp, assumption)+
 
 text{*ORELSE with REPEAT*}
-lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
+lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P;  Suc x < 5\<rbrakk> \<Longrightarrow> R" 
 by (drule mp, (assumption|arith))+
 
 text{*exercise: what's going on here?*}
diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -9,7 +9,7 @@
 numeric literals; default simprules; can re-orient
 *}
 
-lemma "#2 * m = m + m"
+lemma "2 * m = m + m"
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};
@@ -17,10 +17,10 @@
 
 consts h :: "nat \<Rightarrow> nat"
 recdef h "{}"
-"h i = (if i = #3 then #2 else i)"
+"h i = (if i = 3 then 2 else i)"
 
 text{*
-@{term"h #3 = #2"}
+@{term"h 3 = 2"}
 @{term"h i  = i"}
 *}
 
@@ -83,7 +83,7 @@
 *}
 
 
-lemma "(n-#2)*(n+#2) = n*n - (#4::nat)"
+lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
 apply (clarsimp split: nat_diff_split)
  --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (subgoal_tac "n=0 | n=1", force, arith)
@@ -167,7 +167,7 @@
 lemma "abs (x+y) \<le> abs x + abs (y :: int)"
 by arith
 
-lemma "abs (#2*x) = #2 * abs (x :: int)"
+lemma "abs (2*x) = 2 * abs (x :: int)"
 by (simp add: zabs_def) 
 
 text {*REALS
@@ -205,10 +205,10 @@
 \rulename{real_add_divide_distrib}
 *}
 
-lemma "#3/#4 < (#7/#8 :: real)"
+lemma "3/4 < (7/8 :: real)"
 by simp 
 
-lemma "P ((#3/#4) * (#8/#15 :: real))"
+lemma "P ((3/4) * (8/15 :: real))"
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};
@@ -218,7 +218,7 @@
 *};
 oops
 
-lemma "(#3/#4) * (#8/#15) < (x :: real)"
+lemma "(3/4) * (8/15) < (x :: real)"
 txt{*
 @{subgoals[display,indent=0,margin=65]}
 *};
@@ -228,7 +228,7 @@
 *};
 oops
 
-lemma "(#3/#4) * (#10^#15) < (x :: real)"
+lemma "(3/4) * (10^15) < (x :: real)"
 apply simp 
 oops
 
diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Types/Records.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -52,10 +52,10 @@
 
 constdefs 
   pt1 :: point
-   "pt1 == (| Xcoord = #999, Ycoord = #23 |)"
+   "pt1 == (| Xcoord = 999, Ycoord = 23 |)"
 
   pt2 :: "(| Xcoord :: int, Ycoord :: int |)" 
-   "pt2 == (| Xcoord = #-45, Ycoord = #97 |)" 
+   "pt2 == (| Xcoord = -45, Ycoord = 97 |)" 
 
 
 subsubsection {* Some lemmas about records *}
@@ -89,7 +89,7 @@
 
 constdefs 
   cpt1 :: cpoint
-   "cpt1 == (| Xcoord = #999, Ycoord = #23, col = Green |)"
+   "cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
 
 
 subsection {* Generic operations *}
@@ -121,7 +121,7 @@
   setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"
    "setX r a == r (| Xcoord := a |)"
   extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"
-   "extendpt ext == (| Xcoord = #15, Ycoord = 0, ... = ext |)"
+   "extendpt ext == (| Xcoord = 15, Ycoord = 0, ... = ext |)"
      text{*not sure what this is for!*}
 
 
@@ -129,7 +129,7 @@
  \medskip Concrete records are type instances of record schemes.
 *}
 
-lemma "getX (| Xcoord = #64, Ycoord = #36 |) = #64"
+lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64"
 by (simp add: getX_def) 
 
 
@@ -138,7 +138,7 @@
 
 constdefs
   incX :: "('a::more) point_scheme \<Rightarrow> 'a point_scheme"
-  "incX r == \<lparr>Xcoord = (Xcoord r) + #1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
+  "incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
 
 constdefs
   setGreen :: "[colour, ('a::more) point_scheme] \<Rightarrow> cpoint"
@@ -147,11 +147,11 @@
 
 text {* works (I think) for ALL extensions of type point? *}
 
-lemma "incX r = setX r ((getX r) + #1)"
+lemma "incX r = setX r ((getX r) + 1)"
 by (simp add: getX_def setX_def incX_def)
 
 text {* An equivalent definition. *}
-lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + #1\<rparr>"
+lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>"
 by (simp add: incX_def)
 
 
@@ -160,7 +160,7 @@
  Functions on @{text point} schemes work for type @{text cpoint} as
  well.  *}
 
-lemma "getX \<lparr>Xcoord = #23, Ycoord = #10, col = Blue\<rparr> = #23"
+lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23"
 by (simp add: getX_def)
 
 
@@ -170,8 +170,8 @@
  Function @{term setX} can be applied to type @{typ cpoint}, not just type
  @{typ point}, and returns a result of the same type!  *}
 
-lemma "setX \<lparr>Xcoord = #12, Ycoord = 0, col = Blue\<rparr> #23 =  
-            \<lparr>Xcoord = #23, Ycoord = 0, col = Blue\<rparr>"
+lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 =  
+            \<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>"
 by (simp add: setX_def)