1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 14 13:46:03 2006 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 14 13:46:05 2006 +0200
     1.3 @@ -470,6 +470,76 @@
     1.4  \end{warn}
     1.5  
     1.6  
     1.7 +\subsubsection{Classes}
     1.8 +
     1.9 +A special case of locales are type classes. Type classes
    1.10 +consist of a locale with \emph{exactly one} type variable
    1.11 +and an corresponding axclass.
    1.12 +
    1.13 +\indexisarcmd{class}\indexisarcmd{print-classes}
    1.14 +\begin{matharray}{rcl}
    1.15 +  \isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\
    1.16 +  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    1.17 +  \isarcmd{print_classes}^* & : & \isarkeep{theory~|~proof} \\
    1.18 +\end{matharray}
    1.19 +
    1.20 +\begin{rail}
    1.21 +  'class' name '=' classexpr
    1.22 +  ;
    1.23 +  'instance' (instarity | instsubsort)
    1.24 +  ;
    1.25 +  'print\_classes'
    1.26 +  ;
    1.27 +
    1.28 +  classexpr: ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+))
    1.29 +  ;
    1.30 +  instarity: (axmdecl)? (nameref '::' arity + 'and') (axmdecl prop +)?
    1.31 +  ;
    1.32 +  instsubsort: nameref ('<' | subseteq) sort
    1.33 +  ;
    1.34 +  superclassexpr: nameref | (nameref '+' superclassexpr)
    1.35 +  ;
    1.36 +\end{rail}
    1.37 +
    1.38 +\begin{descr}
    1.39 +
    1.40 +\item [$\CLASS~c = superclasses~+~body$] defines a new class $c$,
    1.41 +  inheriting from $superclasses$. Simultaneously, a locale
    1.42 +  named $c$ is introduces, inheriting from the locales
    1.43 +  corresponding to $superclasses$; also, an axclass
    1.44 +  named $c$, inheriting from the axclasses corresponding to
    1.45 +  $superclasses$. $\FIXESNAME$ in $body$ are lifted
    1.46 +  to the theory toplevel, constraining
    1.47 +  the free type variable to sort $c$ and stripping local syntax.
    1.48 +  $\ASSUMESNAME$ in $body$ are also lifted, 
    1.49 +  constraining
    1.50 +  the free type variable to sort $c$.
    1.51 +
    1.52 +\item [$\INSTANCE~a: \vec{arity}~\vec{defs}$]
    1.53 +  sets up a goal stating type arities.  The proof would usually
    1.54 +  proceed by $intro_classes$, and then establish the characteristic theorems
    1.55 +  of the type classes involved.
    1.56 +  The $defs$, if given, must correspond to the class parameters
    1.57 +  involved in the $arities$ and are introduces in the theory
    1.58 +  before proof. Name and attributes given after the $\INSTANCE$
    1.59 +  command refer to \emph{all} definitions as a whole.
    1.60 +  After finishing the proof, the theory will be
    1.61 +  augmented by a type signature declaration corresponding to the
    1.62 +  resulting theorems.
    1.63 +  
    1.64 +\item [$\INSTANCE~c \subseteq \vec{c}$] sets up a
    1.65 +  goal stating 
    1.66 +  the interpretation of the locale corresponding to $c$
    1.67 +  in the merge of all locales corresponding to $\vec{c}$.
    1.68 +  After finishing the proof, it is automatically lifted to
    1.69 +  prove the additional class relation $c \subseteq \vec{c}$.
    1.70 +
    1.71 +\item [$\isarkeyword{print_classes}$] prints the names of all classes
    1.72 +  in the current theory together with some additonal data.
    1.73 +
    1.74 +\end{descr}
    1.75 +
    1.76 +
    1.77  \section{Derived proof schemes}
    1.78  
    1.79  \subsection{Generalized elimination}\label{sec:obtain}
    1.80 @@ -1126,7 +1196,7 @@
    1.81    (\S\ref{sec:pure-meth-att}).
    1.82  
    1.83  \item [$contradiction$] solves some goal by contradiction, deriving any result
    1.84 -  from both $\neg A$ and $A$.  Chained facts, which are guaranteed to
    1.85 +  from both $\lnot A$ and $A$.  Chained facts, which are guaranteed to
    1.86    participate, may appear in either order.
    1.87  
    1.88  \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
    1.89 @@ -1265,7 +1335,7 @@
    1.90    Classical reasoner at the same time.  Non-conditional rules result in a
    1.91    ``safe'' introduction and elimination pair; conditional ones are considered
    1.92    ``unsafe''.  Rules with negative conclusion are automatically inverted
    1.93 -  (using $\neg$ elimination internally).
    1.94 +  (using $\lnot$ elimination internally).
    1.95  
    1.96    The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only,
    1.97    and omits the Simplifier declaration.
    1.98 @@ -1284,7 +1354,7 @@
    1.99  \begin{descr}
   1.100  
   1.101  \item [$swapped$] turns an introduction rule into an elimination, by resolving
   1.102 -  with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
   1.103 +  with the classical swap principle $(\lnot B \Imp A) \Imp (\lnot A \Imp B)$.
   1.104  
   1.105  \end{descr}
   1.106  

     2.1 --- a/doc-src/isar.sty	Mon Aug 14 13:46:03 2006 +0200
     2.2 +++ b/doc-src/isar.sty	Mon Aug 14 13:46:05 2006 +0200
     2.3 @@ -82,6 +82,7 @@
     2.4  \newcommand{\LEMMAS}{\isarkeyword{lemmas}}
     2.5  \newcommand{\THEOREMS}{\isarkeyword{theorems}}
     2.6  \newcommand{\LOCALE}{\isarkeyword{locale}}
     2.7 +\newcommand{\CLASS}{\isarkeyword{class}}
     2.8  \newcommand{\TEXT}{\isarkeyword{text}}
     2.9  \newcommand{\TXT}{\isarkeyword{txt}}
    2.10  \newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}