doc-src/IsarRef/Thy/Generic.thy

--- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 14:27:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:03:31 2011 +0200
@@ -64,6 +64,8 @@
     @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
     @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
     @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
+    @{method_def intro} & : & @{text method} \\
+    @{method_def elim} & : & @{text method} \\
     @{method_def succeed} & : & @{text method} \\
     @{method_def fail} & : & @{text method} \\
   \end{matharray}
@@ -73,6 +75,8 @@
     ;
     (@@{method erule} | @@{method drule} | @@{method frule})
       ('(' @{syntax nat} ')')? @{syntax thmrefs}
+    ;
+    (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
   "}
 
   \begin{description}
@@ -103,6 +107,12 @@
   the plain @{method rule} method, with forward chaining of current
   facts.
 
+  \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.
+
   \item @{method succeed} yields a single (unchanged) result; it is
   the identity of the ``@{text ","}'' method combinator (cf.\
   \secref{sec:proof-meth}).
@@ -879,6 +889,39 @@
 *}
 
 
+subsection {* Structured methods *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{method_def rule} & : & @{text method} \\
+    @{method_def contradiction} & : & @{text method} \\
+  \end{matharray}
+
+  @{rail "
+    @@{method rule} @{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.
+
+  \end{description}
+*}
+
+
 subsection {* Automated methods *}
 
 text {*
@@ -1041,47 +1084,6 @@
 *}
 
 
-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 {*