src/HOL/Isar_examples/BasicLogic.thy
changeset 7480 0a0e0dbe1269
parent 7449 ebd975549ffe
child 7604 55566b9ec7d7
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:12:15 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 04 21:13:01 1999 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    then; show "B & A";
     1.5    proof;
     1.6      assume A B;
     1.7 -    show ??thesis; ..;
     1.8 +    show ?thesis; ..;
     1.9    qed;
    1.10  qed;
    1.11  
    1.12 @@ -123,8 +123,8 @@
    1.13    then; show "EX x. P(x)";
    1.14    proof (rule exE);
    1.15      fix a;
    1.16 -    assume "P(f(a))" (is "P(??witness)");
    1.17 -    show ??thesis; by (rule exI [of P ??witness]);
    1.18 +    assume "P(f(a))" (is "P(?witness)");
    1.19 +    show ?thesis; by (rule exI [of P ?witness]);
    1.20    qed;
    1.21  qed;
    1.22  
    1.23 @@ -135,7 +135,7 @@
    1.24    proof;
    1.25      fix a;
    1.26      assume "P(f(a))";
    1.27 -    show ??thesis; ..;
    1.28 +    show ?thesis; ..;
    1.29    qed;
    1.30  qed;
    1.31