--- 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"
--- 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
--- 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]}
--- 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?*}
--- 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
--- 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)