print_simpset / print_claset command;
authorwenzelm
Tue Apr 04 22:16:11 2000 +0200 (2000-04-04 ago)
changeset 86674230d17073ea
parent 8666 6c21e6f91804
child 8668 ee73e7b26686
print_simpset / print_claset command;
doc-src/IsarRef/generic.tex
src/Provers/classical.ML
src/Provers/simplifier.ML
     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
     2.1 --- a/src/Provers/classical.ML	Tue Apr 04 18:08:08 2000 +0200
     2.2 +++ b/src/Provers/classical.ML	Tue Apr 04 22:16:11 2000 +0200
     2.3 @@ -1181,4 +1181,16 @@
     2.4  val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
     2.5  
     2.6  
     2.7 +
     2.8 +(** outer syntax **)
     2.9 +
    2.10 +val print_clasetP =
    2.11 +  OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    2.12 +    OuterSyntax.Keyword.diag
    2.13 +    (Scan.succeed (Toplevel.keep
    2.14 +      (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))));
    2.15 +
    2.16 +val _ = OuterSyntax.add_parsers [print_clasetP];
    2.17 +
    2.18 +
    2.19  end;
     3.1 --- a/src/Provers/simplifier.ML	Tue Apr 04 18:08:08 2000 +0200
     3.2 +++ b/src/Provers/simplifier.ML	Tue Apr 04 22:16:11 2000 +0200
     3.3 @@ -550,6 +550,17 @@
     3.4    in setup @ method_setup [] @ [init_ss] end;
     3.5  
     3.6  
     3.7 +
     3.8 +(** outer syntax **)
     3.9 +
    3.10 +val print_simpsetP =
    3.11 +  OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
    3.12 +    OuterSyntax.Keyword.diag
    3.13 +    (Scan.succeed (Toplevel.keep
    3.14 +      (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of))));
    3.15 +
    3.16 +val _ = OuterSyntax.add_parsers [print_simpsetP];
    3.17 +
    3.18  end;
    3.19  
    3.20