src/HOL/Isar_Examples/Group.thy
 changeset 55656 eb07b0acbebc parent 37671 fa53d267dab3 child 58614 7338eb25226c
```     1.1 --- a/src/HOL/Isar_Examples/Group.thy	Fri Feb 21 17:06:48 2014 +0100
1.2 +++ b/src/HOL/Isar_Examples/Group.thy	Fri Feb 21 18:23:11 2014 +0100
1.3 @@ -27,19 +27,19 @@
1.4  proof -
1.5    have "x * inverse x = 1 * (x * inverse x)"
1.6      by (simp only: group_left_one)
1.7 -  also have "... = 1 * x * inverse x"
1.8 +  also have "\<dots> = 1 * x * inverse x"
1.9      by (simp only: group_assoc)
1.10 -  also have "... = inverse (inverse x) * inverse x * x * inverse x"
1.11 +  also have "\<dots> = inverse (inverse x) * inverse x * x * inverse x"
1.12      by (simp only: group_left_inverse)
1.13 -  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
1.14 +  also have "\<dots> = inverse (inverse x) * (inverse x * x) * inverse x"
1.15      by (simp only: group_assoc)
1.16 -  also have "... = inverse (inverse x) * 1 * inverse x"
1.17 +  also have "\<dots> = inverse (inverse x) * 1 * inverse x"
1.18      by (simp only: group_left_inverse)
1.19 -  also have "... = inverse (inverse x) * (1 * inverse x)"
1.20 +  also have "\<dots> = inverse (inverse x) * (1 * inverse x)"
1.21      by (simp only: group_assoc)
1.22 -  also have "... = inverse (inverse x) * inverse x"
1.23 +  also have "\<dots> = inverse (inverse x) * inverse x"
1.24      by (simp only: group_left_one)
1.25 -  also have "... = 1"
1.26 +  also have "\<dots> = 1"
1.27      by (simp only: group_left_inverse)
1.28    finally show ?thesis .
1.29  qed
1.30 @@ -52,11 +52,11 @@
1.31  proof -
1.32    have "x * 1 = x * (inverse x * x)"
1.33      by (simp only: group_left_inverse)
1.34 -  also have "... = x * inverse x * x"
1.35 +  also have "\<dots> = x * inverse x * x"
1.36      by (simp only: group_assoc)
1.37 -  also have "... = 1 * x"
1.38 +  also have "\<dots> = 1 * x"
1.39      by (simp only: group_right_inverse)
1.40 -  also have "... = x"
1.41 +  also have "\<dots> = x"
1.42      by (simp only: group_left_one)
1.43    finally show ?thesis .
1.44  qed
1.45 @@ -92,25 +92,25 @@
1.46    note calculation = this
1.47      -- {* first calculational step: init calculation register *}
1.48
1.49 -  have "... = x * inverse x * x"
1.50 +  have "\<dots> = x * inverse x * x"
1.51      by (simp only: group_assoc)
1.52
1.53    note calculation = trans [OF calculation this]
1.54      -- {* general calculational step: compose with transitivity rule *}
1.55
1.56 -  have "... = 1 * x"
1.57 +  have "\<dots> = 1 * x"
1.58      by (simp only: group_right_inverse)
1.59
1.60    note calculation = trans [OF calculation this]
1.61      -- {* general calculational step: compose with transitivity rule *}
1.62
1.63 -  have "... = x"
1.64 +  have "\<dots> = x"
1.65      by (simp only: group_left_one)
1.66
1.67    note calculation = trans [OF calculation this]
1.68 -    -- {* final calculational step: compose with transitivity rule ... *}
1.69 +    -- {* final calculational step: compose with transitivity rule \dots *}
1.70    from calculation
1.71 -    -- {* ... and pick up the final result *}
1.72 +    -- {* \dots\ and pick up the final result *}
1.73
1.74    show ?thesis .
1.75  qed
1.76 @@ -168,13 +168,13 @@
1.77  proof -
1.78    have "1 = x * inverse x"
1.79      by (simp only: group_right_inverse)
1.80 -  also have "... = (e * x) * inverse x"
1.81 +  also have "\<dots> = (e * x) * inverse x"
1.82      by (simp only: eq)
1.83 -  also have "... = e * (x * inverse x)"
1.84 +  also have "\<dots> = e * (x * inverse x)"
1.85      by (simp only: group_assoc)
1.86 -  also have "... = e * 1"
1.87 +  also have "\<dots> = e * 1"
1.88      by (simp only: group_right_inverse)
1.89 -  also have "... = e"
1.90 +  also have "\<dots> = e"
1.91      by (simp only: group_right_one)
1.92    finally show ?thesis .
1.93  qed
1.94 @@ -187,13 +187,13 @@
1.95  proof -
1.96    have "inverse x = 1 * inverse x"
1.97      by (simp only: group_left_one)
1.98 -  also have "... = (x' * x) * inverse x"
1.99 +  also have "\<dots> = (x' * x) * inverse x"
1.100      by (simp only: eq)
1.101 -  also have "... = x' * (x * inverse x)"
1.102 +  also have "\<dots> = x' * (x * inverse x)"
1.103      by (simp only: group_assoc)
1.104 -  also have "... = x' * 1"
1.105 +  also have "\<dots> = x' * 1"
1.106      by (simp only: group_right_inverse)
1.107 -  also have "... = x'"
1.108 +  also have "\<dots> = x'"
1.109      by (simp only: group_right_one)
1.110    finally show ?thesis .
1.111  qed
1.112 @@ -207,11 +207,11 @@
1.113      have "(inverse y * inverse x) * (x * y) =
1.114          (inverse y * (inverse x * x)) * y"
1.115        by (simp only: group_assoc)
1.116 -    also have "... = (inverse y * 1) * y"
1.117 +    also have "\<dots> = (inverse y * 1) * y"
1.118        by (simp only: group_left_inverse)
1.119 -    also have "... = inverse y * y"
1.120 +    also have "\<dots> = inverse y * y"
1.121        by (simp only: group_right_one)
1.122 -    also have "... = 1"
1.123 +    also have "\<dots> = 1"
1.124        by (simp only: group_left_inverse)
1.125      finally show ?thesis .
1.126    qed
1.127 @@ -229,15 +229,15 @@
1.128  proof -
1.129    have "x = x * 1"
1.130      by (simp only: group_right_one)
1.131 -  also have "... = x * (inverse y * y)"
1.132 +  also have "\<dots> = x * (inverse y * y)"
1.133      by (simp only: group_left_inverse)
1.134 -  also have "... = x * (inverse x * y)"
1.135 +  also have "\<dots> = x * (inverse x * y)"
1.136      by (simp only: eq)
1.137 -  also have "... = (x * inverse x) * y"
1.138 +  also have "\<dots> = (x * inverse x) * y"
1.139      by (simp only: group_assoc)
1.140 -  also have "... = 1 * y"
1.141 +  also have "\<dots> = 1 * y"
1.142      by (simp only: group_right_inverse)
1.143 -  also have "... = y"
1.144 +  also have "\<dots> = y"
1.145      by (simp only: group_left_one)
1.146    finally show ?thesis .
1.147  qed
```