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

author | wenzelm |

Wed, 01 Sep 1999 21:35:20 +0200 | |

changeset 7433 | 27887c52b9c8 |

parent 7432 | c32a0fd117a0 |

child 7434 | 132e8ed29bd8 |

"this";

--- a/src/HOL/Isar_examples/Group.thy Wed Sep 01 21:35:04 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Wed Sep 01 21:35:20 1999 +0200 @@ -89,25 +89,25 @@ have "x * one = x * (inv x * x)"; by (simp only: group_left_inverse); - note calculation = facts + note calculation = this -- {* first calculational step: init calculation register *}; have "... = x * inv x * x"; by (simp only: group_assoc); - note calculation = trans [OF calculation facts] + note calculation = trans [OF calculation this] -- {* general calculational step: compose with transitivity rule *}; have "... = one * x"; by (simp only: group_right_inverse); - note calculation = trans [OF calculation facts] + note calculation = trans [OF calculation this] -- {* general calculational step: compose with transitivity rule *}; have "... = x"; by (simp only: group_left_unit); - note calculation = trans [OF calculation facts] + note calculation = trans [OF calculation this] -- {* final calculational step: compose with transitivity rule ... *}; from calculation -- {* ... and pick up final result *};