renamed with/APP to of/OF;

--- 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;
 

--- 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 *};