1.1 --- a/doc-src/Classes/Thy/Classes.thy	Mon Feb 22 14:11:03 2010 +0100
     1.2 +++ b/doc-src/Classes/Thy/Classes.thy	Mon Feb 22 17:02:39 2010 +0100
     1.3 @@ -362,17 +362,18 @@
     1.4  
     1.5  text {*
     1.6    \noindent The connection to the type system is done by means
     1.7 -  of a primitive axclass
     1.8 +  of a primitive type class
     1.9  *} (*<*)setup %invisible {* Sign.add_path "foo" *}
    1.10  (*>*)
    1.11 -axclass %quote idem < type
    1.12 -  idem: "f (f x) = f x" (*<*)setup %invisible {* Sign.parent_path *}(*>*)
    1.13 +classes %quote idem < type
    1.14 +(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
    1.15 +setup %invisible {* Sign.parent_path *}(*>*)
    1.16  
    1.17  text {* \noindent together with a corresponding interpretation: *}
    1.18  
    1.19  interpretation %quote idem_class:
    1.20    idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
    1.21 -proof qed (rule idem)
    1.22 +(*<*)proof qed (rule idem)(*>*)
    1.23  
    1.24  text {*
    1.25    \noindent This gives you the full power of the Isabelle module system;
    1.26 @@ -414,8 +415,7 @@
    1.27  subsection {* Derived definitions *}
    1.28  
    1.29  text {*
    1.30 -  Isabelle locales support a concept of local definitions
    1.31 -  in locales:
    1.32 +  Isabelle locales are targets which support local definitions:
    1.33  *}
    1.34  
    1.35  primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where

     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 14:11:03 2010 +0100
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Mon Feb 22 17:02:39 2010 +0100
     2.3 @@ -641,7 +641,7 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \noindent The connection to the type system is done by means
     2.7 -  of a primitive axclass%
     2.8 +  of a primitive type class%
     2.9  \end{isamarkuptext}%
    2.10  \isamarkuptrue%
    2.11  \ %
    2.12 @@ -663,9 +663,8 @@
    2.13  \endisadelimquote
    2.14  %
    2.15  \isatagquote
    2.16 -\isacommand{axclass}\isamarkupfalse%
    2.17 -\ idem\ {\isacharless}\ type\isanewline
    2.18 -\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
    2.19 +\isacommand{classes}\isamarkupfalse%
    2.20 +\ idem\ {\isacharless}\ type%
    2.21  \endisatagquote
    2.22  {\isafoldquote}%
    2.23  %
    2.24 @@ -698,10 +697,7 @@
    2.25  \isatagquote
    2.26  \isacommand{interpretation}\isamarkupfalse%
    2.27  \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
    2.28 -\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
    2.29 -\isacommand{proof}\isamarkupfalse%
    2.30 -\ \isacommand{qed}\isamarkupfalse%
    2.31 -\ {\isacharparenleft}rule\ idem{\isacharparenright}%
    2.32 +\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
    2.33  \endisatagquote
    2.34  {\isafoldquote}%
    2.35  %

     3.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Feb 22 14:11:03 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Feb 22 17:02:39 2010 +0100
     3.3 @@ -738,44 +738,6 @@
     3.4  *}
     3.5  
     3.6  
     3.7 -subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
     3.8 -
     3.9 -text {*
    3.10 -  \begin{matharray}{rcl}
    3.11 -    @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"}
    3.12 -  \end{matharray}
    3.13 -
    3.14 -  Axiomatic type classes are Isabelle/Pure's primitive
    3.15 -  interface to type classes.  For practical
    3.16 -  applications, you should consider using classes
    3.17 -  (cf.~\secref{sec:classes}) which provide high level interface.
    3.18 -
    3.19 -  \begin{rail}
    3.20 -    'axclass' classdecl (axmdecl prop +)
    3.21 -    ;
    3.22 -  \end{rail}
    3.23 -
    3.24 -  \begin{description}
    3.25 -  
    3.26 -  \item @{command "axclass"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n axms"} defines an
    3.27 -  axiomatic type class as the intersection of existing classes, with
    3.28 -  additional axioms holding.  Class axioms may not contain more than
    3.29 -  one type variable.  The class axioms (with implicit sort constraints
    3.30 -  added) are bound to the given names.  Furthermore a class
    3.31 -  introduction rule is generated (being bound as @{text
    3.32 -  c_class.intro}); this rule is employed by method @{method
    3.33 -  intro_classes} to support instantiation proofs of this class.
    3.34 -  
    3.35 -  The ``class axioms'' (which are derived from the internal class
    3.36 -  definition) are stored as theorems according to the given name
    3.37 -  specifications; the name space prefix @{text "c_class"} is added
    3.38 -  here.  The full collection of these facts is also stored as @{text
    3.39 -  c_class.axioms}.
    3.40 -  
    3.41 -  \end{description}
    3.42 -*}
    3.43 -
    3.44 -
    3.45  section {* Unrestricted overloading *}
    3.46  
    3.47  text {*
    3.48 @@ -962,8 +924,9 @@
    3.49  
    3.50    \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
    3.51    relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
    3.52 -  This is done axiomatically!  The @{command_ref "instance"} command
    3.53 -  (see \secref{sec:axclass}) provides a way to introduce proven class
    3.54 +  This is done axiomatically!  The @{command_ref "instance"}
    3.55 +  and @{command_ref "subclass"} command
    3.56 +  (see \secref{sec:class}) provide a way to introduce proven class
    3.57    relations.
    3.58  
    3.59    \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
    3.60 @@ -1021,8 +984,8 @@
    3.61  
    3.62    \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
    3.63    Isabelle's order-sorted signature of types by new type constructor
    3.64 -  arities.  This is done axiomatically!  The @{command_ref "instance"}
    3.65 -  command (see \secref{sec:axclass}) provides a way to introduce
    3.66 +  arities.  This is done axiomatically!  The @{command_ref "instantiation"}
    3.67 +  target (see \secref{sec:class}) provides a way to introduce
    3.68    proven type arities.
    3.69  
    3.70    \end{description}

     4.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 22 14:11:03 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Feb 22 17:02:39 2010 +0100
     4.3 @@ -755,43 +755,6 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  %
     4.7 -\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
     4.8 -}
     4.9 -\isamarkuptrue%
    4.10 -%
    4.11 -\begin{isamarkuptext}%
    4.12 -\begin{matharray}{rcl}
    4.13 -    \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
    4.14 -  \end{matharray}
    4.15 -
    4.16 -  Axiomatic type classes are Isabelle/Pure's primitive
    4.17 -  interface to type classes.  For practical
    4.18 -  applications, you should consider using classes
    4.19 -  (cf.~\secref{sec:classes}) which provide high level interface.
    4.20 -
    4.21 -  \begin{rail}
    4.22 -    'axclass' classdecl (axmdecl prop +)
    4.23 -    ;
    4.24 -  \end{rail}
    4.25 -
    4.26 -  \begin{description}
    4.27 -  
    4.28 -  \item \hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}} defines an
    4.29 -  axiomatic type class as the intersection of existing classes, with
    4.30 -  additional axioms holding.  Class axioms may not contain more than
    4.31 -  one type variable.  The class axioms (with implicit sort constraints
    4.32 -  added) are bound to the given names.  Furthermore a class
    4.33 -  introduction rule is generated (being bound as \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class.
    4.34 -  
    4.35 -  The ``class axioms'' (which are derived from the internal class
    4.36 -  definition) are stored as theorems according to the given name
    4.37 -  specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
    4.38 -  here.  The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
    4.39 -  
    4.40 -  \end{description}%
    4.41 -\end{isamarkuptext}%
    4.42 -\isamarkuptrue%
    4.43 -%
    4.44  \isamarkupsection{Unrestricted overloading%
    4.45  }
    4.46  \isamarkuptrue%
    4.47 @@ -996,8 +959,9 @@
    4.48  
    4.49    \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass
    4.50    relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
    4.51 -  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command
    4.52 -  (see \secref{sec:axclass}) provides a way to introduce proven class
    4.53 +  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
    4.54 +  and \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} command
    4.55 +  (see \secref{sec:class}) provide a way to introduce proven class
    4.56    relations.
    4.57  
    4.58    \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
    4.59 @@ -1056,8 +1020,8 @@
    4.60  
    4.61    \item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} augments
    4.62    Isabelle's order-sorted signature of types by new type constructor
    4.63 -  arities.  This is done axiomatically!  The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
    4.64 -  command (see \secref{sec:axclass}) provides a way to introduce
    4.65 +  arities.  This is done axiomatically!  The \indexref{}{command}{instantiation}\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
    4.66 +  target (see \secref{sec:class}) provides a way to introduce
    4.67    proven type arities.
    4.68  
    4.69    \end{description}%