1.1 --- a/doc-src/Classes/classes.tex	Tue May 26 13:40:49 2009 +0200
     1.2 +++ b/doc-src/Classes/classes.tex	Tue May 26 13:40:50 2009 +0200
     1.3 @@ -21,12 +21,11 @@
     1.4  \maketitle
     1.5  
     1.6  \begin{abstract}
     1.7 -  \noindent This tutorial introduces the look-and-feel of Isar type classes
     1.8 -  to the end-user; Isar type classes are a convenient mechanism
     1.9 -  for organizing specifications, overcoming some drawbacks
    1.10 -  of raw axiomatic type classes. Essentially, they combine
    1.11 -  an operational aspect (in the manner of Haskell) with
    1.12 -  a logical aspect, both managed uniformly.
    1.13 +  \noindent This tutorial introduces the look-and-feel of
    1.14 +  Isar type classes to the end-user.  Isar type classes
    1.15 +  are a convenient mechanism for organizing specifications.
    1.16 +  Essentially, they combine an operational aspect (in the
    1.17 +  manner of Haskell) with a logical aspect, both managed uniformly.
    1.18  \end{abstract}
    1.19  
    1.20  \thispagestyle{empty}\clearpage

     2.1 --- a/doc-src/Functions/functions.tex	Tue May 26 13:40:49 2009 +0200
     2.2 +++ b/doc-src/Functions/functions.tex	Tue May 26 13:40:50 2009 +0200
     2.3 @@ -16,7 +16,6 @@
     2.4  \newcommand{\isasymLOCALE}{\cmd{locale}}
     2.5  \newcommand{\isasymINCLUDES}{\cmd{includes}}
     2.6  \newcommand{\isasymDATATYPE}{\cmd{datatype}}
     2.7 -\newcommand{\isasymAXCLASS}{\cmd{axclass}}
     2.8  \newcommand{\isasymDEFINES}{\cmd{defines}}
     2.9  \newcommand{\isasymNOTES}{\cmd{notes}}
    2.10  \newcommand{\isasymCLASS}{\cmd{class}}

     3.1 --- a/doc-src/IsarOverview/Isar/Calc.thy	Tue May 26 13:40:49 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,49 +0,0 @@
     3.4 -theory Calc imports Main begin
     3.5 -
     3.6 -subsection{* Chains of equalities *}
     3.7 -
     3.8 -axclass
     3.9 -  group < zero, plus, minus
    3.10 -  assoc:       "(x + y) + z = x + (y + z)"
    3.11 -  left_0:      "0 + x = x"
    3.12 -  left_minus:  "-x + x = 0"
    3.13 -
    3.14 -theorem right_minus: "x + -x = (0::'a::group)"
    3.15 -proof -
    3.16 -  have   "x + -x = (-(-x) + -x) + (x + -x)"
    3.17 -    by (simp only: left_0 left_minus)
    3.18 -  also have "... = -(-x) + ((-x + x) + -x)"
    3.19 -    by (simp only: group.assoc)
    3.20 -  also have "... = 0"
    3.21 -    by (simp only: left_0 left_minus)
    3.22 -  finally show ?thesis .
    3.23 -qed
    3.24 -
    3.25 -subsection{* Inequalities and substitution *}
    3.26 -
    3.27 -lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
    3.28 -                 zdiff_zmult_distrib zdiff_zmult_distrib2
    3.29 -declare numeral_2_eq_2[simp]
    3.30 -
    3.31 -
    3.32 -lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
    3.33 -proof -
    3.34 -       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
    3.35 -  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by(simp add:distrib)
    3.36 -  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by(simp add:distrib)
    3.37 -  finally show ?thesis by simp
    3.38 -qed
    3.39 -
    3.40 -
    3.41 -subsection{* More transitivity *}
    3.42 -
    3.43 -lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
    3.44 -      shows "(a,d) \<in> R\<^sup>*"
    3.45 -proof -
    3.46 -       have "(a,b) \<in> R\<^sup>*" ..
    3.47 -  also have "(b,c) \<in> R\<^sup>*" ..
    3.48 -  also have "(c,d) \<in> R\<^sup>*" ..
    3.49 -  finally show ?thesis .
    3.50 -qed
    3.51 -
    3.52 -end
    3.53 \ No newline at end of file

     4.1 --- a/doc-src/manual.bib	Tue May 26 13:40:49 2009 +0200
     4.2 +++ b/doc-src/manual.bib	Tue May 26 13:40:50 2009 +0200
     4.3 @@ -1344,14 +1344,6 @@
     4.4    institution	= {TU Munich},
     4.5    note          = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
     4.6  
     4.7 -@manual{isabelle-axclass,
     4.8 -  author	= {Markus Wenzel},
     4.9 -  title		= {Using Axiomatic Type Classes in {I}sabelle},
    4.10 -  institution	= {TU Munich},
    4.11 -  year          = 2000,
    4.12 -  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
    4.13 -
    4.14 -
    4.15  @InProceedings{Wenzel:1999:TPHOL,
    4.16    author = 	 {Markus Wenzel},
    4.17    title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},