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

2.1 --- a/src/HOL/Isar_examples/Group.thy Thu Jul 01 21:28:49 1999 +0200
2.2 +++ b/src/HOL/Isar_examples/Group.thy Thu Jul 01 21:29:53 1999 +0200
2.3 @@ -95,19 +95,19 @@
2.4 have "... = x * inv x * x";
2.5 by (simp add: group_assoc);
2.6
2.7 - note calculation = trans[APP calculation facts]
2.8 + note calculation = trans[OF calculation facts]
2.9 -- {* general calculational step: compose with transitivity rule *};
2.10
2.11 have "... = one * x";
2.12 by (simp add: group_right_inverse);
2.13
2.14 - note calculation = trans[APP calculation facts]
2.15 + note calculation = trans[OF calculation facts]
2.16 -- {* general calculational step: compose with transitivity rule *};
2.17
2.18 have "... = x";
2.19 by (simp add: group_left_unit);
2.20
2.21 - note calculation = trans[APP calculation facts]
2.22 + note calculation = trans[OF calculation facts]
2.23 -- {* final calculational step: compose with transitivity rule ... *};
2.24 from calculation
2.25 -- {* ... and pick up final result *};