--- a/src/HOL/Isar_examples/BasicLogic.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Sep 04 21:13:01 1999 +0200
@@ -80,7 +80,7 @@
then; show "B & A";
proof;
assume A B;
- show ??thesis; ..;
+ show ?thesis; ..;
qed;
qed;
@@ -123,8 +123,8 @@
then; show "EX x. P(x)";
proof (rule exE);
fix a;
- assume "P(f(a))" (is "P(??witness)");
- show ??thesis; by (rule exI [of P ??witness]);
+ assume "P(f(a))" (is "P(?witness)");
+ show ?thesis; by (rule exI [of P ?witness]);
qed;
qed;
@@ -135,7 +135,7 @@
proof;
fix a;
assume "P(f(a))";
- show ??thesis; ..;
+ show ?thesis; ..;
qed;
qed;
--- a/src/HOL/Isar_examples/Cantor.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Sat Sep 04 21:13:01 1999 +0200
@@ -34,25 +34,25 @@
theorem "EX S. S ~: range(f :: 'a => 'a set)";
proof;
- let ??S = "{x. x ~: f x}";
- show "??S ~: range f";
+ let ?S = "{x. x ~: f x}";
+ show "?S ~: range f";
proof;
- assume "??S : range f";
+ assume "?S : range f";
then; show False;
proof;
fix y;
- assume "??S = f y";
- then; show ??thesis;
+ assume "?S = f y";
+ then; show ?thesis;
proof (rule equalityCE);
- assume y_in_S: "y : ??S";
+ assume y_in_S: "y : ?S";
assume y_in_fy: "y : f y";
from y_in_S; have y_notin_fy: "y ~: f y"; ..;
- from y_notin_fy y_in_fy; show ??thesis; by contradiction;
+ from y_notin_fy y_in_fy; show ?thesis; by contradiction;
next;
- assume y_notin_S: "y ~: ??S";
+ assume y_notin_S: "y ~: ?S";
assume y_notin_fy: "y ~: f y";
from y_notin_S; have y_in_fy: "y : f y"; ..;
- from y_notin_fy y_in_fy; show ??thesis; by contradiction;
+ from y_notin_fy y_in_fy; show ?thesis; by contradiction;
qed;
qed;
qed;
@@ -67,23 +67,23 @@
theorem "EX S. S ~: range(f :: 'a => 'a set)";
proof;
- let ??S = "{x. x ~: f x}";
- show "??S ~: range f";
+ let ?S = "{x. x ~: f x}";
+ show "?S ~: range f";
proof;
- assume "??S : range f";
+ assume "?S : range f";
thus False;
proof;
fix y;
- assume "??S = f y";
- thus ??thesis;
+ assume "?S = f y";
+ thus ?thesis;
proof (rule equalityCE);
assume "y : f y";
- assume "y : ??S"; hence "y ~: f y"; ..;
- thus ??thesis; by contradiction;
+ assume "y : ?S"; hence "y ~: f y"; ..;
+ thus ?thesis; by contradiction;
next;
assume "y ~: f y";
- assume "y ~: ??S"; hence "y : f y"; ..;
- thus ??thesis; by contradiction;
+ assume "y ~: ?S"; hence "y : f y"; ..;
+ thus ?thesis; by contradiction;
qed;
qed;
qed;
--- a/src/HOL/Isar_examples/ExprCompiler.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Sat Sep 04 21:13:01 1999 +0200
@@ -100,30 +100,30 @@
*};
lemma exec_append:
- "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
-proof (induct ??P xs type: list);
- show "??P []"; by simp;
+ "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
+proof (induct ?P xs type: list);
+ show "?P []"; by simp;
fix x xs;
- assume "??P xs";
- show "??P (x # xs)" (is "??Q x");
- proof (induct ??Q x type: instr);
- fix val; show "??Q (Const val)"; by force;
+ assume "?P xs";
+ show "?P (x # xs)" (is "?Q x");
+ proof (induct ?Q x type: instr);
+ fix val; show "?Q (Const val)"; by force;
next;
- fix adr; show "??Q (Load adr)"; by force;
+ fix adr; show "?Q (Load adr)"; by force;
next;
- fix fun; show "??Q (Apply fun)"; by force;
+ fix fun; show "?Q (Apply fun)"; by force;
qed;
qed;
lemma exec_comp:
- "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
-proof (induct ??P e type: expr);
- fix adr; show "??P (Variable adr)"; by force;
+ "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
+proof (induct ?P e type: expr);
+ fix adr; show "?P (Variable adr)"; by force;
next;
- fix val; show "??P (Constant val)"; by force;
+ fix val; show "?P (Constant val)"; by force;
next;
- fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
+ fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
by (force simp add: exec_append);
qed;
--- a/src/HOL/Isar_examples/Group.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Sat Sep 04 21:13:01 1999 +0200
@@ -49,7 +49,7 @@
by (simp only: group_left_unit);
also; have "... = one";
by (simp only: group_left_inverse);
- finally; show ??thesis; .;
+ finally; show ?thesis; .;
qed;
text {*
@@ -67,7 +67,7 @@
by (simp only: group_right_inverse);
also; have "... = x";
by (simp only: group_left_unit);
- finally; show ??thesis; .;
+ finally; show ?thesis; .;
qed;
text {*
@@ -80,7 +80,7 @@
Note that "..." is just a special term binding that happens to be
bound automatically to the argument of the last fact established by
- assume or any local goal. In contrast to ??thesis, "..." is bound
+ assume or any local goal. In contrast to ?thesis, "..." is bound
after the proof is finished.
*};
@@ -112,7 +112,7 @@
from calculation
-- {* ... and pick up final result *};
- show ??thesis; .;
+ show ?thesis; .;
qed;
--- a/src/HOL/Isar_examples/KnasterTarski.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Sat Sep 04 21:13:01 1999 +0200
@@ -37,28 +37,28 @@
theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
proof;
- let ??H = "{u. f u <= u}";
- let ??a = "Inter ??H";
+ let ?H = "{u. f u <= u}";
+ let ?a = "Inter ?H";
assume mono: "mono f";
- show "f ??a = ??a";
+ show "f ?a = ?a";
proof -;
{{;
fix x;
- assume mem: "x : ??H";
- hence "??a <= x"; by (rule Inter_lower);
- with mono; have "f ??a <= f x"; ..;
+ assume mem: "x : ?H";
+ hence "?a <= x"; by (rule Inter_lower);
+ with mono; have "f ?a <= f x"; ..;
also; from mem; have "... <= x"; ..;
- finally; have "f ??a <= x"; .;
+ finally; have "f ?a <= x"; .;
}};
- hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
+ hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
{{;
- also; presume "... <= f ??a";
- finally (order_antisym); show ??thesis; .;
+ also; presume "... <= f ?a";
+ finally (order_antisym); show ?thesis; .;
}};
- from mono ge; have "f (f ??a) <= f ??a"; ..;
- hence "f ??a : ??H"; ..;
- thus "??a <= f ??a"; by (rule Inter_lower);
+ from mono ge; have "f (f ?a) <= f ?a"; ..;
+ hence "f ?a : ?H"; ..;
+ thus "?a <= f ?a"; by (rule Inter_lower);
qed;
qed;
--- a/src/HOL/Isar_examples/MultisetOrder.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Sat Sep 04 21:13:01 1999 +0200
@@ -14,50 +14,50 @@
lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)";
proof;
- let ??R = "mult1 r";
- let ??W = "acc ??R";
+ let ?R = "mult1 r";
+ let ?W = "acc ?R";
{{;
fix M M0 a;
- assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)"
- and M0: "M0 : ??W"
- and acc_hyp: "ALL M. (M, M0) : ??R --> M + {#a#} : ??W";
- have "M0 + {#a#} : ??W";
+ assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
+ and M0: "M0 : ?W"
+ and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
+ have "M0 + {#a#} : ?W";
proof (rule accI [of "M0 + {#a#}"]);
- fix N; assume "(N, M0 + {#a#}) : ??R";
- hence "((EX M. (M, M0) : ??R & N = M + {#a#}) |
+ fix N; assume "(N, M0 + {#a#}) : ?R";
+ hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
by (simp only: less_add_conv);
- thus "N : ??W";
+ thus "N : ?W";
proof (elim exE disjE conjE);
- fix M; assume "(M, M0) : ??R" and N: "N = M + {#a#}";
- from acc_hyp; have "(M, M0) : ??R --> M + {#a#} : ??W"; ..;
- hence "M + {#a#} : ??W"; ..;
- thus "N : ??W"; by (simp only: N);
+ fix M; assume "(M, M0) : ?R" and N: "N = M + {#a#}";
+ from acc_hyp; have "(M, M0) : ?R --> M + {#a#} : ?W"; ..;
+ hence "M + {#a#} : ?W"; ..;
+ thus "N : ?W"; by (simp only: N);
next;
fix K;
assume N: "N = M0 + K";
assume "ALL b. elem K b --> (b, a) : r";
- have "??this --> M0 + K : ??W" (is "??P K");
+ have "?this --> M0 + K : ?W" (is "?P K");
proof (rule multiset_induct [of _ K]);
- from M0; have "M0 + {#} : ??W"; by simp;
- thus "??P {#}"; ..;
+ from M0; have "M0 + {#} : ?W"; by simp;
+ thus "?P {#}"; ..;
- fix K x; assume hyp: "??P K";
- show "??P (K + {#x#})";
+ fix K x; assume hyp: "?P K";
+ show "?P (K + {#x#})";
proof;
assume a: "ALL b. elem (K + {#x#}) b --> (b, a) : r";
hence "(x, a) : r"; by simp;
- with wf_hyp [RS spec]; have b: "ALL M:??W. M + {#x#} : ??W"; ..;
+ with wf_hyp [RS spec]; have b: "ALL M:?W. M + {#x#} : ?W"; ..;
- from a hyp; have "M0 + K : ??W"; by simp;
- with b; have "(M0 + K) + {#x#} : ??W"; ..;
- thus "M0 + (K + {#x#}) : ??W"; by (simp only: union_assoc);
+ from a hyp; have "M0 + K : ?W"; by simp;
+ with b; have "(M0 + K) + {#x#} : ?W"; ..;
+ thus "M0 + (K + {#x#}) : ?W"; by (simp only: union_assoc);
qed;
qed;
- hence "M0 + K : ??W"; ..;
- thus "N : ??W"; by (simp only: N);
+ hence "M0 + K : ?W"; ..;
+ thus "N : ?W"; by (simp only: N);
qed;
qed;
}}; note tedious_reasoning = this;
@@ -65,25 +65,25 @@
assume wf: "wf r";
fix M;
- show "M : ??W";
+ show "M : ?W";
proof (rule multiset_induct [of _ M]);
- show "{#} : ??W";
+ show "{#} : ?W";
proof (rule accI);
- fix b; assume "(b, {#}) : ??R";
- with not_less_empty; show "b : ??W"; by contradiction;
+ fix b; assume "(b, {#}) : ?R";
+ with not_less_empty; show "b : ?W"; by contradiction;
qed;
- fix M a; assume "M : ??W";
- from wf; have "ALL M:??W. M + {#a#} : ??W";
+ fix M a; assume "M : ?W";
+ from wf; have "ALL M:?W. M + {#a#} : ?W";
proof (rule wf_induct [of r]);
- fix a; assume "ALL b. (b, a) : r --> (ALL M:??W. M + {#b#} : ??W)";
- show "ALL M:??W. M + {#a#} : ??W";
+ fix a; assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)";
+ show "ALL M:?W. M + {#a#} : ?W";
proof;
- fix M; assume "M : ??W";
- thus "M + {#a#} : ??W"; by (rule acc_induct) (rule tedious_reasoning);
+ fix M; assume "M : ?W";
+ thus "M + {#a#} : ?W"; by (rule acc_induct) (rule tedious_reasoning);
qed;
qed;
- thus "M + {#a#} : ??W"; ..;
+ thus "M + {#a#} : ?W"; ..;
qed;
qed;
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Sat Sep 04 21:13:01 1999 +0200
@@ -28,21 +28,21 @@
lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
proof;
- assume "t : tiling A" (is "_ : ??T");
- thus "u : ??T --> t Int u = {} --> t Un u : ??T" (is "??P t");
+ assume "t : tiling A" (is "_ : ?T");
+ thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
proof (induct t set: tiling);
- show "??P {}"; by simp;
+ show "?P {}"; by simp;
fix a t;
- assume "a : A" "t : ??T" "??P t" "a <= - t";
- show "??P (a Un t)";
+ assume "a : A" "t : ?T" "?P t" "a <= - t";
+ show "?P (a Un t)";
proof (intro impI);
- assume "u : ??T" "(a Un t) Int u = {}";
- have hyp: "t Un u: ??T"; by blast;
+ assume "u : ?T" "(a Un t) Int u = {}";
+ have hyp: "t Un u: ?T"; by blast;
have "a <= - (t Un u)"; by blast;
- with _ hyp; have "a Un (t Un u) : ??T"; by (rule tiling.Un);
+ with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
- finally; show "... : ??T"; .;
+ finally; show "... : ?T"; .;
qed;
qed;
qed;
@@ -113,41 +113,41 @@
lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
- (is "??P n" is "??B n : ??T");
+ (is "?P n" is "?B n : ?T");
proof (induct n);
- show "??P 0"; by (simp add: below_0 tiling.empty);
+ show "?P 0"; by (simp add: below_0 tiling.empty);
- fix n; assume hyp: "??P n";
- let ??a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
+ fix n; assume hyp: "?P n";
+ let ?a = "{i} Times {2 * n + 1} Un {i} Times {2 * n}";
- have "??B (Suc n) = ??a Un ??B n"; by (simp add: Sigma_Suc Un_assoc);
- also; have "... : ??T";
+ have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc);
+ also; have "... : ?T";
proof (rule tiling.Un);
have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
- also; have "{(i, 2 * n), (i, 2 * n + 1)} = ??a"; by blast;
+ also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
finally; show "... : domino"; .;
- from hyp; show "??B n : ??T"; .;
- show "??a <= - ??B n"; by force;
+ from hyp; show "?B n : ?T"; .;
+ show "?a <= - ?B n"; by force;
qed;
- finally; show "??P (Suc n)"; .;
+ finally; show "?P (Suc n)"; .;
qed;
lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino"
- (is "??P m" is "??B m : ??T");
+ (is "?P m" is "?B m : ?T");
proof (induct m);
- show "??P 0"; by (simp add: below_0 tiling.empty);
+ show "?P 0"; by (simp add: below_0 tiling.empty);
- fix m; assume hyp: "??P m";
- let ??t = "{m} Times below (2 * n)";
+ fix m; assume hyp: "?P m";
+ let ?t = "{m} Times below (2 * n)";
- have "??B (Suc m) = ??t Un ??B m"; by (simp add: Sigma_Suc);
- also; have "... : ??T";
+ have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
+ also; have "... : ?T";
proof (rule tiling_Un [rulify]);
- show "??t : ??T"; by (rule dominoes_tile_row);
- from hyp; show "??B m : ??T"; .;
- show "??t Int ??B m = {}"; by blast;
+ show "?t : ?T"; by (rule dominoes_tile_row);
+ from hyp; show "?B m : ?T"; .;
+ show "?t Int ?B m = {}"; by blast;
qed;
- finally; show "??P (Suc m)"; .;
+ finally; show "?P (Suc m)"; .;
qed;
@@ -155,13 +155,13 @@
proof -;
assume "b < 2";
assume "d : domino";
- thus ??thesis (is "??P d");
+ thus ?thesis (is "?P d");
proof (induct d set: domino);
have b_cases: "b = 0 | b = 1"; by arith;
fix i j;
note [simp] = evnodd_empty evnodd_insert mod_Suc;
- from b_cases; show "??P {(i, j), (i, j + 1)}"; by rule auto;
- from b_cases; show "??P {(i, j), (i + 1, j)}"; by rule auto;
+ from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
+ from b_cases; show "?P {(i, j), (i + 1, j)}"; by rule auto;
qed;
qed;
@@ -175,54 +175,54 @@
section {* Tilings of dominoes *};
-lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ??T ==> ??F t");
+lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
proof -;
- assume "t : ??T";
- thus "??F t";
+ assume "t : ?T";
+ thus "?F t";
proof (induct t set: tiling);
- show "??F {}"; by (rule Finites.emptyI);
- fix a t; assume "??F t";
- assume "a : domino"; hence "??F a"; by (rule domino_finite);
- thus "??F (a Un t)"; by (rule finite_UnI);
+ show "?F {}"; by (rule Finites.emptyI);
+ fix a t; assume "?F t";
+ assume "a : domino"; hence "?F a"; by (rule domino_finite);
+ thus "?F (a Un t)"; by (rule finite_UnI);
qed;
qed;
lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
- (is "t : ??T ==> ??P t");
+ (is "t : ?T ==> ?P t");
proof -;
- assume "t : ??T";
- thus "??P t";
+ assume "t : ?T";
+ thus "?P t";
proof (induct t set: tiling);
- show "??P {}"; by (simp add: evnodd_def);
+ show "?P {}"; by (simp add: evnodd_def);
fix a t;
- let ??e = evnodd;
- assume "a : domino" "t : ??T"
- and hyp: "card (??e t 0) = card (??e t 1)"
+ let ?e = evnodd;
+ assume "a : domino" "t : ?T"
+ and hyp: "card (?e t 0) = card (?e t 1)"
and "a <= - t";
- have card_suc: "!!b. b < 2 ==> card (??e (a Un t) b) = Suc (card (??e t b))";
+ have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
proof -;
fix b; assume "b < 2";
- have "EX i j. ??e a b = {(i, j)}"; by (rule domino_singleton);
- thus "??thesis b";
+ have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
+ thus "?thesis b";
proof (elim exE);
- have "??e (a Un t) b = ??e a b Un ??e t b"; by (rule evnodd_Un);
- also; fix i j; assume "??e a b = {(i, j)}";
- also; have "... Un ??e t b = insert (i, j) (??e t b)"; by simp;
- also; have "card ... = Suc (card (??e t b))";
+ have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
+ also; fix i j; assume "?e a b = {(i, j)}";
+ also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
+ also; have "card ... = Suc (card (?e t b))";
proof (rule card_insert_disjoint);
- show "finite (??e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
- have "(i, j) : ??e a b"; by asm_simp;
- thus "(i, j) ~: ??e t b"; by (force dest: evnoddD);
+ show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
+ have "(i, j) : ?e a b"; by asm_simp;
+ thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
qed;
- finally; show ??thesis; .;
+ finally; show ?thesis; .;
qed;
qed;
- hence "card (??e (a Un t) 0) = Suc (card (??e t 0))"; by simp;
- also; from hyp; have "card (??e t 0) = card (??e t 1)"; .;
- also; from card_suc; have "Suc ... = card (??e (a Un t) 1)"; by simp;
- finally; show "??P (a Un t)"; .;
+ hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
+ also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
+ also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp;
+ finally; show "?P (a Un t)"; .;
qed;
qed;
@@ -236,37 +236,37 @@
theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino";
proof (unfold mutilated_board_def);
- let ??T = "tiling domino";
- let ??t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
- let ??t' = "??t - {(0, 0)}";
- let ??t'' = "??t' - {(2 * m + 1, 2 * n + 1)}";
- show "??t'' ~: ??T";
+ let ?T = "tiling domino";
+ let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))";
+ let ?t' = "?t - {(0, 0)}";
+ let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}";
+ show "?t'' ~: ?T";
proof;
- have t: "??t : ??T"; by (rule dominoes_tile_matrix);
- assume t'': "??t'' : ??T";
+ have t: "?t : ?T"; by (rule dominoes_tile_matrix);
+ assume t'': "?t'' : ?T";
- let ??e = evnodd;
- have fin: "finite (??e ??t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
+ let ?e = evnodd;
+ have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t);
note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
- have "card (??e ??t'' 0) < card (??e ??t' 0)";
+ have "card (?e ?t'' 0) < card (?e ?t' 0)";
proof -;
- have "card (??e ??t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (??e ??t' 0)";
+ have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
proof (rule card_Diff1_less);
- show "finite (??e ??t' 0)"; by (rule finite_subset, rule fin) force;
- show "(2 * m + 1, 2 * n + 1) : ??e ??t' 0"; by simp;
+ show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
+ show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
qed;
- thus ??thesis; by simp;
+ thus ?thesis; by simp;
qed;
- also; have "... < card (??e ??t 0)";
+ also; have "... < card (?e ?t 0)";
proof -;
- have "(0, 0) : ??e ??t 0"; by simp;
- with fin; have "card (??e ??t 0 - {(0, 0)}) < card (??e ??t 0)"; by (rule card_Diff1_less);
- thus ??thesis; by simp;
+ have "(0, 0) : ?e ?t 0"; by simp;
+ with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less);
+ thus ?thesis; by simp;
qed;
- also; from t; have "... = card (??e ??t 1)"; by (rule tiling_domino_01);
- also; have "??e ??t 1 = ??e ??t'' 1"; by simp;
- also; from t''; have "card ... = card (??e ??t'' 0)"; by (rule tiling_domino_01 [RS sym]);
+ also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
+ also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
+ also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]);
finally; show False; ..;
qed;
qed;
--- a/src/HOL/Isar_examples/Summation.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Sat Sep 04 21:13:01 1999 +0200
@@ -46,51 +46,51 @@
theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
- (is "??P n" is "??S n = _");
+ (is "?P n" is "?S n = _");
proof (induct n);
- show "??P 0"; by simp;
+ show "?P 0"; by simp;
fix n;
- have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp;
- also; assume "??S n = n * (n + 1)";
+ have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
+ also; assume "?S n = n * (n + 1)";
also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
- finally; show "??P (Suc n)"; by simp;
+ finally; show "?P (Suc n)"; by simp;
qed;
theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
- (is "??P n" is "??S n = _");
+ (is "?P n" is "?S n = _");
proof (induct n);
- show "??P 0"; by simp;
+ show "?P 0"; by simp;
fix n;
- have "??S (n + 1) = ??S n + 2 * n + 1"; by simp;
- also; assume "??S n = n^2";
+ have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
+ also; assume "?S n = n^2";
also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
- finally; show "??P (Suc n)"; by simp;
+ finally; show "?P (Suc n)"; by simp;
qed;
theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
- (is "??P n" is "??S n = _");
+ (is "?P n" is "?S n = _");
proof (induct n);
- show "??P 0"; by simp;
+ show "?P 0"; by simp;
fix n;
- have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp;
- also; assume "??S n = n * (n + 1) * (2 * n + 1)";
+ have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
+ also; assume "?S n = n * (n + 1) * (2 * n + 1)";
also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
- finally; show "??P (Suc n)"; by simp;
+ finally; show "?P (Suc n)"; by simp;
qed;
theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
- (is "??P n" is "??S n = _");
+ (is "?P n" is "?S n = _");
proof (induct n);
- show "??P 0"; by simp;
+ show "?P 0"; by simp;
fix n;
- have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp;
- also; assume "??S n = (n * (n + 1))^2";
+ have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
+ also; assume "?S n = (n * (n + 1))^2";
also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
- finally; show "??P (Suc n)"; by simp;
+ finally; show "?P (Suc n)"; by simp;
qed;
--- a/src/HOL/ex/Points.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/ex/Points.thy Sat Sep 04 21:13:01 1999 +0200
@@ -94,9 +94,9 @@
text {* equality of records *};
-lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
+lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "?EQ --> _");
proof;
- assume ??EQ;
+ assume ?EQ;
thus "n = n'"; by simp;
qed;