1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Jun 17 10:11:33 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Jun 17 10:34:02 2009 +0200
     1.3 @@ -585,6 +585,7 @@
     1.4      @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
     1.5      @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
     1.6      @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.7 +    @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.8      @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9      @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.10      @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.11 @@ -599,8 +600,12 @@
    1.12      ;
    1.13      'instance'
    1.14      ;
    1.15 +    'instance' nameref '::' arity
    1.16 +    ;
    1.17      'subclass' target? nameref
    1.18      ;
    1.19 +    'instance' nameref ('<' | subseteq) nameref
    1.20 +    ;
    1.21      'print\_classes'
    1.22      ;
    1.23      'class\_deps'
    1.24 @@ -649,12 +654,24 @@
    1.25    the type classes involved.  After finishing the proof, the
    1.26    background theory will be augmented by the proven type arities.
    1.27  
    1.28 +  On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
    1.29 +  s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
    1.30 +  need to specifify operations: one can continue with the
    1.31 +  instantiation proof immediately.
    1.32 +
    1.33    \item @{command "subclass"}~@{text c} in a class context for class
    1.34    @{text d} sets up a goal stating that class @{text c} is logically
    1.35    contained in class @{text d}.  After finishing the proof, class
    1.36    @{text d} is proven to be subclass @{text c} and the locale @{text
    1.37    c} is interpreted into @{text d} simultaneously.
    1.38  
    1.39 +  A weakend form of this is available through a further variant of
    1.40 +  @{command instance}:  @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
    1.41 +  a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference
    1.42 +  to the underlying locales;  this is useful if the properties to prove
    1.43 +  the logical connection are not sufficent on the locale level but on
    1.44 +  the theory level.
    1.45 +
    1.46    \item @{command "print_classes"} prints all classes in the current
    1.47    theory.
    1.48  
    1.49 @@ -703,20 +720,17 @@
    1.50  
    1.51  text {*
    1.52    \begin{matharray}{rcl}
    1.53 -    @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
    1.54 -    @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
    1.55 +    @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"}
    1.56    \end{matharray}
    1.57  
    1.58    Axiomatic type classes are Isabelle/Pure's primitive
    1.59 -  \emph{definitional} interface to type classes.  For practical
    1.60 +  interface to type classes.  For practical
    1.61    applications, you should consider using classes
    1.62    (cf.~\secref{sec:classes}) which provide high level interface.
    1.63  
    1.64    \begin{rail}
    1.65      'axclass' classdecl (axmdecl prop +)
    1.66      ;
    1.67 -    'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
    1.68 -    ;
    1.69    \end{rail}
    1.70  
    1.71    \begin{description}
    1.72 @@ -736,14 +750,6 @@
    1.73    here.  The full collection of these facts is also stored as @{text
    1.74    c_class.axioms}.
    1.75    
    1.76 -  \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
    1.77 -  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
    1.78 -  relation or type arity.  The proof would usually proceed by @{method
    1.79 -  intro_classes}, and then establish the characteristic theorems of
    1.80 -  the type classes involved.  After finishing the proof, the theory
    1.81 -  will be augmented by a type signature declaration corresponding to
    1.82 -  the resulting theorem.
    1.83 -
    1.84    \end{description}
    1.85  *}
    1.86