diff -r af028f35af60 -r eb07b0acbebc src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy Fri Feb 21 17:06:48 2014 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Fri Feb 21 18:23:11 2014 +0100
@@ -27,19 +27,19 @@
proof -
have "x * inverse x = 1 * (x * inverse x)"
by (simp only: group_left_one)
- also have "... = 1 * x * inverse x"
+ also have "\ = 1 * x * inverse x"
by (simp only: group_assoc)
- also have "... = inverse (inverse x) * inverse x * x * inverse x"
+ also have "\ = inverse (inverse x) * inverse x * x * inverse x"
by (simp only: group_left_inverse)
- also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
+ also have "\ = inverse (inverse x) * (inverse x * x) * inverse x"
by (simp only: group_assoc)
- also have "... = inverse (inverse x) * 1 * inverse x"
+ also have "\ = inverse (inverse x) * 1 * inverse x"
by (simp only: group_left_inverse)
- also have "... = inverse (inverse x) * (1 * inverse x)"
+ also have "\ = inverse (inverse x) * (1 * inverse x)"
by (simp only: group_assoc)
- also have "... = inverse (inverse x) * inverse x"
+ also have "\ = inverse (inverse x) * inverse x"
by (simp only: group_left_one)
- also have "... = 1"
+ also have "\ = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
qed
@@ -52,11 +52,11 @@
proof -
have "x * 1 = x * (inverse x * x)"
by (simp only: group_left_inverse)
- also have "... = x * inverse x * x"
+ also have "\ = x * inverse x * x"
by (simp only: group_assoc)
- also have "... = 1 * x"
+ also have "\ = 1 * x"
by (simp only: group_right_inverse)
- also have "... = x"
+ also have "\ = x"
by (simp only: group_left_one)
finally show ?thesis .
qed
@@ -92,25 +92,25 @@
note calculation = this
-- {* first calculational step: init calculation register *}
- have "... = x * inverse x * x"
+ have "\ = x * inverse x * x"
by (simp only: group_assoc)
note calculation = trans [OF calculation this]
-- {* general calculational step: compose with transitivity rule *}
- have "... = 1 * x"
+ have "\ = 1 * x"
by (simp only: group_right_inverse)
note calculation = trans [OF calculation this]
-- {* general calculational step: compose with transitivity rule *}
- have "... = x"
+ have "\ = x"
by (simp only: group_left_one)
note calculation = trans [OF calculation this]
- -- {* final calculational step: compose with transitivity rule ... *}
+ -- {* final calculational step: compose with transitivity rule \dots *}
from calculation
- -- {* ... and pick up the final result *}
+ -- {* \dots\ and pick up the final result *}
show ?thesis .
qed
@@ -168,13 +168,13 @@
proof -
have "1 = x * inverse x"
by (simp only: group_right_inverse)
- also have "... = (e * x) * inverse x"
+ also have "\ = (e * x) * inverse x"
by (simp only: eq)
- also have "... = e * (x * inverse x)"
+ also have "\ = e * (x * inverse x)"
by (simp only: group_assoc)
- also have "... = e * 1"
+ also have "\ = e * 1"
by (simp only: group_right_inverse)
- also have "... = e"
+ also have "\ = e"
by (simp only: group_right_one)
finally show ?thesis .
qed
@@ -187,13 +187,13 @@
proof -
have "inverse x = 1 * inverse x"
by (simp only: group_left_one)
- also have "... = (x' * x) * inverse x"
+ also have "\ = (x' * x) * inverse x"
by (simp only: eq)
- also have "... = x' * (x * inverse x)"
+ also have "\ = x' * (x * inverse x)"
by (simp only: group_assoc)
- also have "... = x' * 1"
+ also have "\ = x' * 1"
by (simp only: group_right_inverse)
- also have "... = x'"
+ also have "\ = x'"
by (simp only: group_right_one)
finally show ?thesis .
qed
@@ -207,11 +207,11 @@
have "(inverse y * inverse x) * (x * y) =
(inverse y * (inverse x * x)) * y"
by (simp only: group_assoc)
- also have "... = (inverse y * 1) * y"
+ also have "\ = (inverse y * 1) * y"
by (simp only: group_left_inverse)
- also have "... = inverse y * y"
+ also have "\ = inverse y * y"
by (simp only: group_right_one)
- also have "... = 1"
+ also have "\ = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
qed
@@ -229,15 +229,15 @@
proof -
have "x = x * 1"
by (simp only: group_right_one)
- also have "... = x * (inverse y * y)"
+ also have "\ = x * (inverse y * y)"
by (simp only: group_left_inverse)
- also have "... = x * (inverse x * y)"
+ also have "\ = x * (inverse x * y)"
by (simp only: eq)
- also have "... = (x * inverse x) * y"
+ also have "\ = (x * inverse x) * y"
by (simp only: group_assoc)
- also have "... = 1 * y"
+ also have "\ = 1 * y"
by (simp only: group_right_inverse)
- also have "... = y"
+ also have "\ = y"
by (simp only: group_left_one)
finally show ?thesis .
qed