# HG changeset patch
# User wenzelm
# Date 930857393 -7200
# Node ID 91a2c8b8269af2e1bf9771813aaabc841f6f4a64
# Parent  ce2b19e4402dc0f9d0bc3d4254fbcf76d1a049b7
renamed with/APP to of/OF;

diff -r ce2b19e4402d -r 91a2c8b8269a src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:28:49 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Thu Jul 01 21:29:53 1999 +0200
@@ -106,7 +106,7 @@
   proof (rule exE);
     fix a;
     assume "P(f(a))" (is "P(??witness)");
-    show ??thesis; by (rule exI [with P ??witness]);
+    show ??thesis; by (rule exI [of P ??witness]);
   qed;
 qed;
 
diff -r ce2b19e4402d -r 91a2c8b8269a src/HOL/Isar_examples/Group.thy
--- a/src/HOL/Isar_examples/Group.thy	Thu Jul 01 21:28:49 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy	Thu Jul 01 21:29:53 1999 +0200
@@ -95,19 +95,19 @@
   have "... = x * inv x * x";
     by (simp add: group_assoc);
 
-  note calculation = trans[APP calculation facts]
+  note calculation = trans[OF calculation facts]
     -- {* general calculational step: compose with transitivity rule *};
 
   have "... = one * x";
     by (simp add: group_right_inverse);
 
-  note calculation = trans[APP calculation facts]
+  note calculation = trans[OF calculation facts]
     -- {* general calculational step: compose with transitivity rule *};
 
   have "... = x";
     by (simp add: group_left_unit);
 
-  note calculation = trans[APP calculation facts]
+  note calculation = trans[OF calculation facts]
     -- {* final calculational step: compose with transitivity rule ... *};
   from calculation
     -- {* ... and pick up final result *};