summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 01 Jul 1999 21:29:53 +0200 | |

changeset 6881 | 91a2c8b8269a |

parent 6880 | ce2b19e4402d |

child 6882 | fe4e3d26fa8f |

renamed with/APP to of/OF;

src/HOL/Isar_examples/BasicLogic.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/Group.thy | file | annotate | diff | comparison | revisions |

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