# HG changeset patch
# User wenzelm
# Date 936214520 -7200
# Node ID 27887c52b9c8d1332ef270ab5c2897f47feecb85
# Parent  c32a0fd117a0ca9f0265b0c239863bf9cee6d988
"this";

diff -r c32a0fd117a0 -r 27887c52b9c8 src/HOL/Isar_examples/Group.thy
--- 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 *};