doc-src/IsarRef/generic.tex
changeset 7167 0b2e3ef1d8f4
parent 7141 a67dde8820c0
child 7175 8263d0b50e12
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Aug 03 13:16:29 1999 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Aug 03 18:56:51 1999 +0200
     1.3 @@ -1,5 +1,76 @@
     1.4  
     1.5 -\chapter{Generic Tools and Packages}
     1.6 +\chapter{Generic Tools and Packages}\label{ch:gen-tools}
     1.7 +
     1.8 +\section{Basic proof methods and attributes}\label{sec:pure-meth}
     1.9 +
    1.10 +\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
    1.11 +\indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
    1.12 +\indexisarmeth{rule}\indexisarmeth{erule}
    1.13 +\begin{matharray}{rcl}
    1.14 +  fail & : & \isarmeth \\
    1.15 +  succeed & : & \isarmeth \\
    1.16 +  - & : & \isarmeth \\
    1.17 +  assumption & : & \isarmeth \\
    1.18 +  finish & : & \isarmeth \\
    1.19 +  fold & : & \isarmeth \\
    1.20 +  unfold & : & \isarmeth \\
    1.21 +  rule & : & \isarmeth \\
    1.22 +  erule^* & : & \isarmeth \\
    1.23 +\end{matharray}
    1.24 +
    1.25 +\begin{rail}
    1.26 +  ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
    1.27 +  ;
    1.28 +\end{rail}
    1.29 +
    1.30 +\begin{descr}
    1.31 +\item [$ $]
    1.32 +\end{descr}
    1.33 +
    1.34 +FIXME
    1.35 +
    1.36 +%FIXME sort
    1.37 +%FIXME thmref (single)
    1.38 +%FIXME var vs. term
    1.39 +
    1.40 +\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
    1.41 +\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
    1.42 +\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
    1.43 +\begin{matharray}{rcl}
    1.44 +  tag & : & \isaratt \\
    1.45 +  untag & : & \isaratt \\
    1.46 +  COMP & : & \isaratt \\
    1.47 +  RS & : & \isaratt \\
    1.48 +  OF & : & \isaratt \\
    1.49 +  where & : & \isaratt \\
    1.50 +  of & : & \isaratt \\
    1.51 +  standard & : & \isaratt \\
    1.52 +  elimify & : & \isaratt \\
    1.53 +  transfer & : & \isaratt \\
    1.54 +  export & : & \isaratt \\
    1.55 +\end{matharray}
    1.56 +
    1.57 +\begin{rail}
    1.58 +  ('tag' | 'untag') (nameref+)
    1.59 +  ;
    1.60 +  ('COMP' | 'RS') nat? thmref
    1.61 +  ;
    1.62 +  'OF' thmrefs
    1.63 +  ;
    1.64 +  'where' (term '=' term * 'and')
    1.65 +  ;
    1.66 +  'of' (inst * ) ('concl:' (inst * ))?
    1.67 +  ;
    1.68 +
    1.69 +  inst: underscore | term
    1.70 +  ;
    1.71 +\end{rail}
    1.72 +
    1.73 +\begin{descr}
    1.74 +\item [$ $]
    1.75 +\end{descr}
    1.76 +
    1.77 +FIXME
    1.78  
    1.79  \section{Axiomatic Type Classes}\label{sec:axclass}
    1.80  
    1.81 @@ -23,7 +94,7 @@
    1.82    ;
    1.83  \end{rail}
    1.84  
    1.85 -\begin{description}
    1.86 +\begin{descr}
    1.87  \item [$\isarkeyword{axclass}~$] FIXME
    1.88  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
    1.89    c@2$] setup up a goal stating the class relation or type arity.  The proof
    1.90 @@ -31,7 +102,7 @@
    1.91    characteristic theorems of the type classes involved.  After finishing the
    1.92    proof the theory will be augmented by a type signature declaration
    1.93    corresponding to the resulting theorem.
    1.94 -\end{description}
    1.95 +\end{descr}
    1.96  
    1.97  
    1.98  
    1.99 @@ -49,9 +120,9 @@
   1.100    
   1.101  %\end{rail}
   1.102  
   1.103 -%\begin{description}
   1.104 +%\begin{descr}
   1.105  %\item [$ $]
   1.106 -%\end{description}
   1.107 +%\end{descr}
   1.108  
   1.109  
   1.110  %%% Local Variables: