--- 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
--- 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}}
--- 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
--- 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},