# HG changeset patch
# User wenzelm
# Date 1212441084 -7200
# Node ID c4eaa7140532fe730165827c030f22a94af8b1b7
# Parent  3ff111ed85a1d86bb860caaa21b618285a6838af
moved subst/hypsubst to "Basic proof tools";
tuned;

diff -r 3ff111ed85a1 -r c4eaa7140532 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 02 22:50:54 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 02 23:11:24 2008 +0200
@@ -156,9 +156,9 @@
   \item [@{attribute rotated}~@{text n}] rotate the premises of a
   theorem by @{text n} (default 1).
 
-  \item [@{attribute Pure.elim_format}] turns a destruction rule into
-  elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow>
-  (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
+  \item [@{attribute (Pure) elim_format}] turns a destruction rule
+  into elimination rule format, by resolving with the rule @{prop
+  "PROP A \<Longrightarrow> (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}.
   
   Note that the Classical Reasoner (\secref{sec:classical}) provides
   its own version of this operation.
@@ -175,6 +175,72 @@
 *}
 
 
+subsection {* Low-level equational reasoning *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{method_def subst} & : & \isarmeth \\
+    @{method_def hypsubst} & : & \isarmeth \\
+    @{method_def split} & : & \isarmeth \\
+  \end{matharray}
+
+  \begin{rail}
+    'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
+    ;
+    'split' ('(' 'asm' ')')? thmrefs
+    ;
+  \end{rail}
+
+  These methods provide low-level facilities for equational reasoning
+  that are intended for specialized applications only.  Normally,
+  single step calculations would be performed in a structured text
+  (see also \secref{sec:calculation}), while the Simplifier methods
+  provide the canonical way for automated normalization (see
+  \secref{sec:simplifier}).
+
+  \begin{descr}
+
+  \item [@{method subst}~@{text eq}] performs a single substitution
+  step using rule @{text eq}, which may be either a meta or object
+  equality.
+
+  \item [@{method subst}~@{text "(asm) eq"}] substitutes in an
+  assumption.
+
+  \item [@{method subst}~@{text "(i \<dots> j) eq"}] performs several
+  substitutions in the conclusion. The numbers @{text i} to @{text j}
+  indicate the positions to substitute at.  Positions are ordered from
+  the top of the term tree moving down from left to right. For
+  example, in @{text "(a + b) + (c + d)"} there are three positions
+  where commutativity of @{text "+"} is applicable: 1 refers to the
+  whole term, 2 to @{text "a + b"} and 3 to @{text "c + d"}.
+
+  If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
+  (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
+  assume all substitutions are performed simultaneously.  Otherwise
+  the behaviour of @{text subst} is not specified.
+
+  \item [@{method subst}~@{text "(asm) (i \<dots> j) eq"}] performs the
+  substitutions in the assumptions.  Positions @{text "1 \<dots> i\<^sub>1"}
+  refer to assumption 1, positions @{text "i\<^sub>1 + 1 \<dots> i\<^sub>2"}
+  to assumption 2, and so on.
+
+  \item [@{method hypsubst}] performs substitution using some
+  assumption; this only works for equations of the form @{text "x =
+  t"} where @{text x} is a free or bound variable.
+
+  \item [@{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] performs
+  single-step case splitting using the given rules.  By default,
+  splitting is performed in the conclusion of a goal; the @{text
+  "(asm)"} option indicates to operate on assumptions instead.
+  
+  Note that the @{method simp} method already involves repeated
+  application of split rules as declared in the current context.
+
+  \end{descr}
+*}
+
+
 subsection {* Further tactic emulations \label{sec:tactics} *}
 
 text {*
@@ -485,72 +551,6 @@
 *}
 
 
-subsection {* Low-level equational reasoning *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{method_def subst}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{method_def hypsubst}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{method_def split}@{text "\<^sup>*"} & : & \isarmeth \\
-  \end{matharray}
-
-  \begin{rail}
-    'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
-    ;
-    'split' ('(' 'asm' ')')? thmrefs
-    ;
-  \end{rail}
-
-  These methods provide low-level facilities for equational reasoning
-  that are intended for specialized applications only.  Normally,
-  single step calculations would be performed in a structured text
-  (see also \secref{sec:calculation}), while the Simplifier methods
-  provide the canonical way for automated normalization (see
-  \secref{sec:simplifier}).
-
-  \begin{descr}
-
-  \item [@{method subst}~@{text eq}] performs a single substitution
-  step using rule @{text eq}, which may be either a meta or object
-  equality.
-
-  \item [@{method subst}~@{text "(asm) eq"}] substitutes in an
-  assumption.
-
-  \item [@{method subst}~@{text "(i \<dots> j) eq"}] performs several
-  substitutions in the conclusion. The numbers @{text i} to @{text j}
-  indicate the positions to substitute at.  Positions are ordered from
-  the top of the term tree moving down from left to right. For
-  example, in @{text "(a + b) + (c + d)"} there are three positions
-  where commutativity of @{text "+"} is applicable: 1 refers to the
-  whole term, 2 to @{text "a + b"} and 3 to @{text "c + d"}.
-
-  If the positions in the list @{text "(i \<dots> j)"} are non-overlapping
-  (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may
-  assume all substitutions are performed simultaneously.  Otherwise
-  the behaviour of @{text subst} is not specified.
-
-  \item [@{method subst}~@{text "(asm) (i \<dots> j) eq"}] performs the
-  substitutions in the assumptions.  Positions @{text "1 \<dots> i\<^sub>1"}
-  refer to assumption 1, positions @{text "i\<^sub>1 + 1 \<dots> i\<^sub>2"}
-  to assumption 2, and so on.
-
-  \item [@{method hypsubst}] performs substitution using some
-  assumption; this only works for equations of the form @{text "x =
-  t"} where @{text x} is a free or bound variable.
-
-  \item [@{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] performs
-  single-step case splitting using the given rules.  By default,
-  splitting is performed in the conclusion of a goal; the @{text
-  "(asm)"} option indicates to operate on assumptions instead.
-  
-  Note that the @{method simp} method already involves repeated
-  application of split rules as declared in the current context.
-
-  \end{descr}
-*}
-
-
 section {* The Classical Reasoner \label{sec:classical} *}
 
 subsection {* Basic methods *}
@@ -761,7 +761,7 @@
 *}
 
 
-section {* General logic setup \label{sec:object-logic} *}
+section {* Object-logic setup \label{sec:object-logic} *}
 
 text {*
   \begin{matharray}{rcl}