expand_classes renamed to intro_classes;
authorwenzelm
Wed Aug 25 20:46:40 1999 +0200 (1999-08-25)
changeset 73561714c91b8729
parent 7355 4c43090659ca
child 7357 d0e16da40ea2
expand_classes renamed to intro_classes;
doc-src/IsarRef/generic.tex
src/HOL/Isar_examples/Group.thy
     1.1 --- a/doc-src/IsarRef/generic.tex	Wed Aug 25 20:45:19 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Wed Aug 25 20:46:40 1999 +0200
     1.3 @@ -194,11 +194,11 @@
     1.4  
     1.5  \section{Axiomatic Type Classes}\label{sec:axclass}
     1.6  
     1.7 -\indexisarcmd{axclass}\indexisarcmd{instance}
     1.8 +\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
     1.9  \begin{matharray}{rcl}
    1.10    \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
    1.11    \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    1.12 -  expand_classes & : & \isarmeth \\
    1.13 +  intro_classes & : & \isarmeth \\
    1.14  \end{matharray}
    1.15  
    1.16  Axiomatic type classes are provided by Isabelle/Pure as a purely
    1.17 @@ -222,18 +222,17 @@
    1.18    holding.  Class axioms may not contain more than one type variable.  The
    1.19    class axioms (with implicit sort constraints added) are bound to the given
    1.20    names.  Furthermore a class introduction rule is generated, which is
    1.21 -  employed by method $expand_classes$ in support instantiation proofs of this
    1.22 +  employed by method $intro_classes$ in support instantiation proofs of this
    1.23    class.
    1.24    
    1.25  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
    1.26    (\vec s)c$] setup up a goal stating the class relation or type arity.  The
    1.27 -  proof would usually proceed by the $expand_classes$ method, and then
    1.28 +  proof would usually proceed by the $intro_classes$ method, and then
    1.29    establish the characteristic theorems of the type classes involved.  After
    1.30    finishing the proof the theory will be augmented by a type signature
    1.31    declaration corresponding to the resulting theorem.
    1.32 -\item [Method $expand_classes$] iteratively expands the class introduction
    1.33 +\item [Method $intro_classes$] iteratively expands the class introduction
    1.34    rules
    1.35 -%FIXME intro classIs etc;
    1.36  \end{descr}
    1.37  
    1.38  See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
     2.1 --- a/src/HOL/Isar_examples/Group.thy	Wed Aug 25 20:45:19 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/Group.thy	Wed Aug 25 20:46:40 1999 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4  *};
     2.5  
     2.6  instance group < monoid;
     2.7 -  by (expand_classes,
     2.8 +  by (intro_classes,
     2.9         rule group_assoc,
    2.10         rule group_left_unit,
    2.11         rule group_right_unit);