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