src/HOL/Isar_examples/BasicLogic.thy
changeset 6881 91a2c8b8269a
parent 6746 cf6ad8d22793
child 6892 4a905b4a39c8
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:28:49 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:29:53 1999 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    proof (rule exE);
     1.5      fix a;
     1.6      assume "P(f(a))" (is "P(??witness)");
     1.7 -    show ??thesis; by (rule exI [with P ??witness]);
     1.8 +    show ??thesis; by (rule exI [of P ??witness]);
     1.9    qed;
    1.10  qed;
    1.11