moved section "Proof method expressions" to proof chapter;
minor rearrangement of proof sections;

--- a/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:34:55 2008 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:37:18 2008 +0100
@@ -100,11 +100,11 @@
 
   \item [@{method succeed}] yields a single (unchanged) result; it is
   the identity of the ``@{text ","}'' method combinator (cf.\
-  \secref{sec:syn-meth}).
+  \secref{sec:proof-meth}).
 
   \item [@{method fail}] yields an empty result sequence; it is the
   identity of the ``@{text "|"}'' method combinator (cf.\
-  \secref{sec:syn-meth}).
+  \secref{sec:proof-meth}).
 
   \end{descr}
 

--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:34:55 2008 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:37:18 2008 +0100
@@ -262,6 +262,51 @@
 *}
 
 
+subsection {* Term patterns and declarations \label{sec:term-decls} *}
+
+text {*
+  Wherever explicit propositions (or term fragments) occur in a proof
+  text, casual binding of schematic term variables may be given
+  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
+  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
+
+  \indexouternonterm{termpat}\indexouternonterm{proppat}
+  \begin{rail}
+    termpat: '(' ('is' term +) ')'
+    ;
+    proppat: '(' ('is' prop +) ')'
+    ;
+  \end{rail}
+
+  \medskip Declarations of local variables @{text "x :: \<tau>"} and
+  logical propositions @{text "a : \<phi>"} represent different views on
+  the same principle of introducing a local scope.  In practice, one
+  may usually omit the typing of \railnonterm{vars} (due to
+  type-inference), and the naming of propositions (due to implicit
+  references of current facts).  In any case, Isar proof elements
+  usually admit to introduce multiple such items simultaneously.
+
+  \indexouternonterm{vars}\indexouternonterm{props}
+  \begin{rail}
+    vars: (name+) ('::' type)?
+    ;
+    props: thmdecl? (prop proppat? +)
+    ;
+  \end{rail}
+
+  The treatment of multiple declarations corresponds to the
+  complementary focus of \railnonterm{vars} versus
+  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
+  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
+  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
+  Isar language elements that refer to \railnonterm{vars} or
+  \railnonterm{props} typically admit separate typings or namings via
+  another level of iteration, with explicit @{keyword_ref "and"}
+  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
+  \secref{sec:proof-context}.
+*}
+
+
 subsection {* Mixfix annotations *}
 
 text {*
@@ -314,7 +359,7 @@
   pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
   @{text "m > n"} works by attaching concrete notation only to the
   innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
-  instead.  If a term has fewer argument than specified in the mixfix
+  instead.  If a term has fewer arguments than specified in the mixfix
   template, the concrete syntax is ignored.
 
   \medskip A mixfix template may also contain additional directives
@@ -366,69 +411,22 @@
   For example, the template @{text "(_ +/ _)"} specifies an infix
   operator.  There are two argument positions; the delimiter @{text
   "+"} is preceded by a space and followed by a space or line break;
-  the entire phrase is a pretty printing block.  
+  the entire phrase is a pretty printing block.
 
   The general idea of pretty printing with blocks and breaks is also
   described in \cite{paulson-ml2}.
 *}
 
 
-subsection {* Proof methods \label{sec:syn-meth} *}
-
-text {*
-  Proof methods are either basic ones, or expressions composed of
-  methods via ``@{verbatim ","}'' (sequential composition),
-  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
-  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
-  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
-  sub-goals, with default @{text "n = 1"}).  In practice, proof
-  methods are usually just a comma separated list of
-  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
-  parentheses may be dropped for single method specifications (with no
-  arguments).
-
-  \indexouternonterm{method}
-  \begin{rail}
-    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
-    ;
-    methods: (nameref args | method) + (',' | '|')
-    ;
-  \end{rail}
-
-  Proper Isar proof methods do \emph{not} admit arbitrary goal
-  addressing, but refer either to the first sub-goal or all sub-goals
-  uniformly.  The goal restriction operator ``@{text "[n]"}''
-  evaluates a method expression within a sandbox consisting of the
-  first @{text n} sub-goals (which need to exist).  For example, the
-  method ``@{text "simp_all[3]"}'' simplifies the first three
-  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
-  new goals that emerge from applying rule @{text "foo"} to the
-  originally first one.
-
-  Improper methods, notably tactic emulations, offer a separate
-  low-level goal addressing scheme as explicit argument to the
-  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
-  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
-  "n"}.
-
-  \indexouternonterm{goalspec}
-  \begin{rail}
-    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
-    ;
-  \end{rail}
-*}
-
-
 subsection {* Attributes and theorems \label{sec:syn-att} *}
 
-text {*
-  Attributes (and proof methods, see \secref{sec:syn-meth}) have their
-  own ``semi-inner'' syntax, in the sense that input conforming to
-  \railnonterm{args} below is parsed by the attribute a second time.
-  The attribute argument specifications may be any sequence of atomic
-  entities (identifiers, strings etc.), or properly bracketed argument
-  lists.  Below \railqtok{atom} refers to any atomic entity, including
-  any \railtok{keyword} conforming to \railtok{symident}.
+text {* Attributes have their own ``semi-inner'' syntax, in the sense
+  that input conforming to \railnonterm{args} below is parsed by the
+  attribute a second time.  The attribute argument specifications may
+  be any sequence of atomic entities (identifiers, strings etc.), or
+  properly bracketed argument lists.  Below \railqtok{atom} refers to
+  any atomic entity, including any \railtok{keyword} conforming to
+  \railtok{symident}.
 
   \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   \begin{rail}
@@ -459,7 +457,7 @@
 
   \item literal fact propositions using @{syntax_ref altstring} syntax
   @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
-  @{method_ref fact} in \secref{sec:pure-meth-att}).
+  @{method_ref fact}).
 
   \end{enumerate}
 
@@ -498,49 +496,4 @@
   \end{rail}
 *}
 
-
-subsection {* Term patterns and declarations \label{sec:term-decls} *}
-
-text {*
-  Wherever explicit propositions (or term fragments) occur in a proof
-  text, casual binding of schematic term variables may be given
-  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
-  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
-
-  \indexouternonterm{termpat}\indexouternonterm{proppat}
-  \begin{rail}
-    termpat: '(' ('is' term +) ')'
-    ;
-    proppat: '(' ('is' prop +) ')'
-    ;
-  \end{rail}
-
-  \medskip Declarations of local variables @{text "x :: \<tau>"} and
-  logical propositions @{text "a : \<phi>"} represent different views on
-  the same principle of introducing a local scope.  In practice, one
-  may usually omit the typing of \railnonterm{vars} (due to
-  type-inference), and the naming of propositions (due to implicit
-  references of current facts).  In any case, Isar proof elements
-  usually admit to introduce multiple such items simultaneously.
-
-  \indexouternonterm{vars}\indexouternonterm{props}
-  \begin{rail}
-    vars: (name+) ('::' type)?
-    ;
-    props: thmdecl? (prop proppat? +)
-    ;
-  \end{rail}
-
-  The treatment of multiple declarations corresponds to the
-  complementary focus of \railnonterm{vars} versus
-  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
-  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
-  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
-  Isar language elements that refer to \railnonterm{vars} or
-  \railnonterm{props} typically admit separate typings or namings via
-  another level of iteration, with explicit @{keyword_ref "and"}
-  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
-  \secref{sec:proof-context}.
-*}
-
 end

--- a/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:34:55 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:37:18 2008 +0100
@@ -42,7 +42,9 @@
 *}
 
 
-section {* Context elements \label{sec:proof-context} *}
+section {* Statements *}
+
+subsection {* Context elements \label{sec:proof-context} *}
 
 text {*
   \begin{matharray}{rcl}
@@ -127,7 +129,77 @@
 *}
 
 
-section {* Facts and forward chaining *}
+subsection {* Term abbreviations \label{sec:term-abbrev} *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
+    @{keyword_def "is"} & : & syntax \\
+  \end{matharray}
+
+  Abbreviations may be either bound by explicit @{command
+  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
+  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
+  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
+  bind extra-logical term variables, which may be either named
+  schematic variables of the form @{text ?x}, or nameless dummies
+  ``@{variable _}'' (underscore). Note that in the @{command "let"}
+  form the patterns occur on the left-hand side, while the @{keyword
+  "is"} patterns are in postfix position.
+
+  Polymorphism of term bindings is handled in Hindley-Milner style,
+  similar to ML.  Type variables referring to local assumptions or
+  open goal statements are \emph{fixed}, while those of finished
+  results or bound by @{command "let"} may occur in \emph{arbitrary}
+  instances later.  Even though actual polymorphism should be rarely
+  used in practice, this mechanism is essential to achieve proper
+  incremental type-inference, as the user proceeds to build up the
+  Isar proof text from left to right.
+
+  \medskip Term abbreviations are quite different from local
+  definitions as introduced via @{command "def"} (see
+  \secref{sec:proof-context}).  The latter are visible within the
+  logic as actual equations, while abbreviations disappear during the
+  input process just after type checking.  Also note that @{command
+  "def"} does not support polymorphism.
+
+  \begin{rail}
+    'let' ((term + 'and') '=' term + 'and')
+    ;  
+  \end{rail}
+
+  The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
+  or \railnonterm{proppat} (see \secref{sec:term-decls}).
+
+  \begin{descr}
+
+  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
+  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
+  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
+  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
+
+  \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
+  "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
+  preceding statement.  Also note that @{keyword "is"} is not a
+  separate command, but part of others (such as @{command "assume"},
+  @{command "have"} etc.).
+
+  \end{descr}
+
+  Some \emph{implicit} term abbreviations\index{term abbreviations}
+  for goals and facts are available as well.  For any open goal,
+  @{variable_ref thesis} refers to its object-level statement,
+  abstracted over any meta-level parameters (if present).  Likewise,
+  @{variable_ref this} is bound for fact statements resulting from
+  assumptions or finished goals.  In case @{variable this} refers to
+  an object-logic statement that is an application @{text "f t"}, then
+  @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
+  (three dots).  The canonical application of this convenience are
+  calculational proofs (see \secref{sec:calculation}).
+*}
+
+
+subsection {* Facts and forward chaining *}
 
 text {*
   \begin{matharray}{rcl}
@@ -215,7 +287,7 @@
 *}
 
 
-section {* Goal statements \label{sec:goals} *}
+subsection {* Goals \label{sec:goals} *}
 
 text {*
   \begin{matharray}{rcl}
@@ -366,7 +438,55 @@
 *}
 
 
-section {* Initial and terminal proof steps \label{sec:proof-steps} *}
+section {* Refinement steps *}
+
+subsection {* Proof method expressions \label{sec:proof-meth} *}
+
+text {*
+  Proof methods are either basic ones, or expressions composed of
+  methods via ``@{verbatim ","}'' (sequential composition),
+  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
+  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
+  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
+  sub-goals, with default @{text "n = 1"}).  In practice, proof
+  methods are usually just a comma separated list of
+  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
+  parentheses may be dropped for single method specifications (with no
+  arguments).
+
+  \indexouternonterm{method}
+  \begin{rail}
+    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
+    ;
+    methods: (nameref args | method) + (',' | '|')
+    ;
+  \end{rail}
+
+  Proper Isar proof methods do \emph{not} admit arbitrary goal
+  addressing, but refer either to the first sub-goal or all sub-goals
+  uniformly.  The goal restriction operator ``@{text "[n]"}''
+  evaluates a method expression within a sandbox consisting of the
+  first @{text n} sub-goals (which need to exist).  For example, the
+  method ``@{text "simp_all[3]"}'' simplifies the first three
+  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
+  new goals that emerge from applying rule @{text "foo"} to the
+  originally first one.
+
+  Improper methods, notably tactic emulations, offer a separate
+  low-level goal addressing scheme as explicit argument to the
+  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
+  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
+  "n"}.
+
+  \indexouternonterm{goalspec}
+  \begin{rail}
+    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
+    ;
+  \end{rail}
+*}
+
+
+subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
 
 text {*
   \begin{matharray}{rcl}
@@ -479,7 +599,7 @@
 *}
 
 
-section {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
+subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
 
 text {*
   The following proof methods and attributes refer to basic logical
@@ -626,119 +746,7 @@
 *}
 
 
-section {* Term abbreviations \label{sec:term-abbrev} *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
-    @{keyword_def "is"} & : & syntax \\
-  \end{matharray}
-
-  Abbreviations may be either bound by explicit @{command
-  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
-  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
-  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
-  bind extra-logical term variables, which may be either named
-  schematic variables of the form @{text ?x}, or nameless dummies
-  ``@{variable _}'' (underscore). Note that in the @{command "let"}
-  form the patterns occur on the left-hand side, while the @{keyword
-  "is"} patterns are in postfix position.
-
-  Polymorphism of term bindings is handled in Hindley-Milner style,
-  similar to ML.  Type variables referring to local assumptions or
-  open goal statements are \emph{fixed}, while those of finished
-  results or bound by @{command "let"} may occur in \emph{arbitrary}
-  instances later.  Even though actual polymorphism should be rarely
-  used in practice, this mechanism is essential to achieve proper
-  incremental type-inference, as the user proceeds to build up the
-  Isar proof text from left to right.
-
-  \medskip Term abbreviations are quite different from local
-  definitions as introduced via @{command "def"} (see
-  \secref{sec:proof-context}).  The latter are visible within the
-  logic as actual equations, while abbreviations disappear during the
-  input process just after type checking.  Also note that @{command
-  "def"} does not support polymorphism.
-
-  \begin{rail}
-    'let' ((term + 'and') '=' term + 'and')
-    ;  
-  \end{rail}
-
-  The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
-  or \railnonterm{proppat} (see \secref{sec:term-decls}).
-
-  \begin{descr}
-
-  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
-  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
-  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
-  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
-
-  \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
-  "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
-  preceding statement.  Also note that @{keyword "is"} is not a
-  separate command, but part of others (such as @{command "assume"},
-  @{command "have"} etc.).
-
-  \end{descr}
-
-  Some \emph{implicit} term abbreviations\index{term abbreviations}
-  for goals and facts are available as well.  For any open goal,
-  @{variable_ref thesis} refers to its object-level statement,
-  abstracted over any meta-level parameters (if present).  Likewise,
-  @{variable_ref this} is bound for fact statements resulting from
-  assumptions or finished goals.  In case @{variable this} refers to
-  an object-logic statement that is an application @{text "f t"}, then
-  @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
-  (three dots).  The canonical application of this convenience are
-  calculational proofs (see \secref{sec:calculation}).
-*}
-
-
-section {* Block structure *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
-    @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
-    @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
-  \end{matharray}
-
-  While Isar is inherently block-structured, opening and closing
-  blocks is mostly handled rather casually, with little explicit
-  user-intervention.  Any local goal statement automatically opens
-  \emph{two} internal blocks, which are closed again when concluding
-  the sub-proof (by @{command "qed"} etc.).  Sections of different
-  context within a sub-proof may be switched via @{command "next"},
-  which is just a single block-close followed by block-open again.
-  The effect of @{command "next"} is to reset the local proof context;
-  there is no goal focus involved here!
-
-  For slightly more advanced applications, there are explicit block
-  parentheses as well.  These typically achieve a stronger forward
-  style of reasoning.
-
-  \begin{descr}
-
-  \item [@{command "next"}] switches to a fresh block within a
-  sub-proof, resetting the local context to the initial one.
-
-  \item [@{command "{"} and @{command "}"}] explicitly open and close
-  blocks.  Any current facts pass through ``@{command "{"}''
-  unchanged, while ``@{command "}"}'' causes any result to be
-  \emph{exported} into the enclosing context.  Thus fixed variables
-  are generalized, assumptions discharged, and local definitions
-  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
-  of @{command "assume"} and @{command "presume"} in this mode of
-  forward reasoning --- in contrast to plain backward reasoning with
-  the result exported at @{command "show"} time.
-
-  \end{descr}
-*}
-
-
-section {* Emulating tactic scripts \label{sec:tactic-commands} *}
+subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
 
 text {*
   The Isar provides separate commands to accommodate tactic-style
@@ -814,6 +822,48 @@
 *}
 
 
+section {* Block structure *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
+    @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
+    @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
+  \end{matharray}
+
+  While Isar is inherently block-structured, opening and closing
+  blocks is mostly handled rather casually, with little explicit
+  user-intervention.  Any local goal statement automatically opens
+  \emph{two} internal blocks, which are closed again when concluding
+  the sub-proof (by @{command "qed"} etc.).  Sections of different
+  context within a sub-proof may be switched via @{command "next"},
+  which is just a single block-close followed by block-open again.
+  The effect of @{command "next"} is to reset the local proof context;
+  there is no goal focus involved here!
+
+  For slightly more advanced applications, there are explicit block
+  parentheses as well.  These typically achieve a stronger forward
+  style of reasoning.
+
+  \begin{descr}
+
+  \item [@{command "next"}] switches to a fresh block within a
+  sub-proof, resetting the local context to the initial one.
+
+  \item [@{command "{"} and @{command "}"}] explicitly open and close
+  blocks.  Any current facts pass through ``@{command "{"}''
+  unchanged, while ``@{command "}"}'' causes any result to be
+  \emph{exported} into the enclosing context.  Thus fixed variables
+  are generalized, assumptions discharged, and local definitions
+  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
+  of @{command "assume"} and @{command "presume"} in this mode of
+  forward reasoning --- in contrast to plain backward reasoning with
+  the result exported at @{command "show"} time.
+
+  \end{descr}
+*}
+
+
 section {* Omitting proofs *}
 
 text {*
@@ -1036,6 +1086,7 @@
   \end{descr}
 *}
 
+
 section {* Proof by cases and induction \label{sec:cases-induct} *}
 
 subsection {* Rule contexts *}