# HG changeset patch
# User haftmann
# Date 1243338050 -7200
# Node ID cf75908fd3c331171096e3a25cb37ffb5080b4dd
# Parent  0f8cb37bcafd297f090ad2b3fb4c896cdc077c41
weakend references to old axclass

diff -r 0f8cb37bcafd -r cf75908fd3c3 doc-src/Classes/classes.tex
--- a/doc-src/Classes/classes.tex	Tue May 26 13:40:49 2009 +0200
+++ b/doc-src/Classes/classes.tex	Tue May 26 13:40:50 2009 +0200
@@ -21,12 +21,11 @@
 \maketitle
 
 \begin{abstract}
-  \noindent This tutorial introduces the look-and-feel of Isar type classes
-  to the end-user; Isar type classes are a convenient mechanism
-  for organizing specifications, overcoming some drawbacks
-  of raw axiomatic type classes. Essentially, they combine
-  an operational aspect (in the manner of Haskell) with
-  a logical aspect, both managed uniformly.
+  \noindent This tutorial introduces the look-and-feel of
+  Isar type classes to the end-user.  Isar type classes
+  are a convenient mechanism for organizing specifications.
+  Essentially, they combine an operational aspect (in the
+  manner of Haskell) with a logical aspect, both managed uniformly.
 \end{abstract}
 
 \thispagestyle{empty}\clearpage
diff -r 0f8cb37bcafd -r cf75908fd3c3 doc-src/Functions/functions.tex
--- a/doc-src/Functions/functions.tex	Tue May 26 13:40:49 2009 +0200
+++ b/doc-src/Functions/functions.tex	Tue May 26 13:40:50 2009 +0200
@@ -16,7 +16,6 @@
 \newcommand{\isasymLOCALE}{\cmd{locale}}
 \newcommand{\isasymINCLUDES}{\cmd{includes}}
 \newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymAXCLASS}{\cmd{axclass}}
 \newcommand{\isasymDEFINES}{\cmd{defines}}
 \newcommand{\isasymNOTES}{\cmd{notes}}
 \newcommand{\isasymCLASS}{\cmd{class}}
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
diff -r 0f8cb37bcafd -r cf75908fd3c3 doc-src/manual.bib
--- a/doc-src/manual.bib	Tue May 26 13:40:49 2009 +0200
+++ b/doc-src/manual.bib	Tue May 26 13:40:50 2009 +0200
@@ -1344,14 +1344,6 @@
   institution	= {TU Munich},
   note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
 
-@manual{isabelle-axclass,
-  author	= {Markus Wenzel},
-  title		= {Using Axiomatic Type Classes in {I}sabelle},
-  institution	= {TU Munich},
-  year          = 2000,
-  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
-
-
 @InProceedings{Wenzel:1999:TPHOL,
   author = 	 {Markus Wenzel},
   title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},