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