diff -r 0f8cb37bcafd -r cf75908fd3c3 doc-src/IsarOverview/Isar/Calc.thy
--- a/doc-src/IsarOverview/Isar/Calc.thy	Tue May 26 13:40:49 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-theory Calc imports Main begin
-
-subsection{* Chains of equalities *}
-
-axclass
-  group < zero, plus, minus
-  assoc:       "(x + y) + z = x + (y + z)"
-  left_0:      "0 + x = x"
-  left_minus:  "-x + x = 0"
-
-theorem right_minus: "x + -x = (0::'a::group)"
-proof -
-  have   "x + -x = (-(-x) + -x) + (x + -x)"
-    by (simp only: left_0 left_minus)
-  also have "... = -(-x) + ((-x + x) + -x)"
-    by (simp only: group.assoc)
-  also have "... = 0"
-    by (simp only: left_0 left_minus)
-  finally show ?thesis .
-qed
-
-subsection{* Inequalities and substitution *}
-
-lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
-                 zdiff_zmult_distrib zdiff_zmult_distrib2
-declare numeral_2_eq_2[simp]
-
-
-lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
-proof -
-       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
-  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by(simp add:distrib)
-  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by(simp add:distrib)
-  finally show ?thesis by simp
-qed
-
-
-subsection{* More transitivity *}
-
-lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
-      shows "(a,d) \<in> R\<^sup>*"
-proof -
-       have "(a,b) \<in> R\<^sup>*" ..
-  also have "(b,c) \<in> R\<^sup>*" ..
-  also have "(c,d) \<in> R\<^sup>*" ..
-  finally show ?thesis .
-qed
-
-end
\ No newline at end of file