renamed with/APP to of/OF;
authorwenzelm
Thu Jul 01 21:29:53 1999 +0200 (1999-07-01)
changeset 688191a2c8b8269a
parent 6880 ce2b19e4402d
child 6882 fe4e3d26fa8f
renamed with/APP to of/OF;
src/HOL/Isar_examples/BasicLogic.thy
src/HOL/Isar_examples/Group.thy
     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 *};