--- a/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 20:15:47 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 20:23:05 2011 +0200
@@ -875,47 +875,6 @@
illustrative purposes: the Classical Reasoner already swaps rules
internally as explained above.
- \end{description} *}
-
-
-subsection {* Basic methods *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def rule} & : & @{text method} \\
- @{method_def contradiction} & : & @{text method} \\
- @{method_def intro} & : & @{text method} \\
- @{method_def elim} & : & @{text method} \\
- \end{matharray}
-
- @{rail "
- (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
- "}
-
- \begin{description}
-
- \item @{method rule} as offered by the Classical Reasoner is a
- refinement over the primitive one (see \secref{sec:pure-meth-att}).
- Both versions essentially work the same, but the classical version
- observes the classical rule context in addition to that of
- Isabelle/Pure.
-
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
-
- \item @{method contradiction} solves some goal by contradiction,
- deriving any result from both @{text "\<not> A"} and @{text A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
-
- \item @{method intro} and @{method elim} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
-
\end{description}
*}
@@ -1009,6 +968,47 @@
*}
+subsection {* Structured proof methods *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def rule} & : & @{text method} \\
+ @{method_def contradiction} & : & @{text method} \\
+ @{method_def intro} & : & @{text method} \\
+ @{method_def elim} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail "
+ (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
+ "}
+
+ \begin{description}
+
+ \item @{method rule} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item @{method contradiction} solves some goal by contradiction,
+ deriving any result from both @{text "\<not> A"} and @{text A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \item @{method intro} and @{method elim} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
+ \end{description}
+*}
+
+
section {* Object-logic setup \label{sec:object-logic} *}
text {*
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:15:47 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:23:05 2011 +0200
@@ -1311,63 +1311,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Basic methods%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
- \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
- \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
- \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@bar
-\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
- refinement over the primitive one (see \secref{sec:pure-meth-att}).
- Both versions essentially work the same, but the classical version
- observes the classical rule context in addition to that of
- Isabelle/Pure.
-
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
-
- \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
- deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
-
- \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsubsection{Automated methods%
}
\isamarkuptrue%
@@ -1578,6 +1521,62 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Structured proof methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
+ \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
+ \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
+ \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{3}{}
+\rail@bar
+\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
+ deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Object-logic setup \label{sec:object-logic}%
}
\isamarkuptrue%