doc-src/IsarRef/generic.tex
changeset 8667 4230d17073ea
parent 8638 21cb46716f32
child 8704 f76f41f24c44
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Apr 04 18:08:08 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Apr 04 22:16:11 2000 +0200
     1.3 @@ -417,8 +417,10 @@
     1.4  
     1.5  \subsection{Declaring rules}
     1.6  
     1.7 +\indexisarcmd{print-simpset}
     1.8  \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
     1.9  \begin{matharray}{rcl}
    1.10 +  print_simpset & : & \isarkeep{theory~|~proof} \\
    1.11    simp & : & \isaratt \\
    1.12    split & : & \isaratt \\
    1.13    cong & : & \isaratt \\
    1.14 @@ -430,6 +432,9 @@
    1.15  \end{rail}
    1.16  
    1.17  \begin{descr}
    1.18 +\item [$print_simpset$] prints the collection of rules declared to the
    1.19 +  Simplifier, which is also known as ``simpset'' internally
    1.20 +  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
    1.21  \item [$simp$] declares simplification rules.
    1.22  \item [$split$] declares split rules.
    1.23  \item [$cong$] declares congruence rules.
    1.24 @@ -572,9 +577,11 @@
    1.25  
    1.26  \subsection{Declaring rules}\label{sec:classical-mod}
    1.27  
    1.28 +\indexisarcmd{print-claset}
    1.29  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
    1.30  \indexisaratt{iff}\indexisaratt{delrule}
    1.31  \begin{matharray}{rcl}
    1.32 +  print_claset & : & \isarkeep{theory~|~proof} \\
    1.33    intro & : & \isaratt \\
    1.34    elim & : & \isaratt \\
    1.35    dest & : & \isaratt \\
    1.36 @@ -589,6 +596,9 @@
    1.37  \end{rail}
    1.38  
    1.39  \begin{descr}
    1.40 +\item [$print_claset$] prints the collection of rules declared to the
    1.41 +  Classical Reasoner, which is also known as ``simpset'' internally
    1.42 +  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
    1.43  \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
    1.44    destruct rules, respectively.  By default, rules are considered as
    1.45    \emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as