tuned;
authorwenzelm
Mon Sep 04 17:06:45 2006 +0200 (2006-09-04)
changeset 20472e993073eda4c
parent 20471 ffafbd4103c0
child 20473 7ef72f030679
tuned;
doc-src/IsarImplementation/IsaMakefile
doc-src/IsarImplementation/Thy/ROOT.ML
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/document/session.tex
doc-src/IsarImplementation/Thy/document/tactic.tex
doc-src/IsarImplementation/Thy/isar.thy
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/proof.thy
doc-src/IsarImplementation/Thy/tactic.thy
doc-src/IsarImplementation/implementation.tex
     1.1 --- a/doc-src/IsarImplementation/IsaMakefile	Mon Sep 04 16:28:36 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/IsaMakefile	Mon Sep 04 17:06:45 2006 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  Thy: $(LOG)/Pure-Thy.gz
     1.6  
     1.7 -$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy \
     1.8 +$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/base.thy Thy/integration.thy Thy/isar.thy \
     1.9    Thy/locale.thy Thy/logic.thy Thy/prelim.thy Thy/proof.thy Thy/tactic.thy \
    1.10    Thy/ML.thy Thy/setup.ML
    1.11  	@$(USEDIR) Pure Thy
     2.1 --- a/doc-src/IsarImplementation/Thy/ROOT.ML	Mon Sep 04 16:28:36 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Mon Sep 04 17:06:45 2006 +0200
     2.3 @@ -5,6 +5,7 @@
     2.4  use_thy "logic";
     2.5  use_thy "tactic";
     2.6  use_thy "proof";
     2.7 +use_thy "isar";
     2.8  use_thy "locale";
     2.9  use_thy "integration";
    2.10  use_thy "ML";
     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Sep 04 16:28:36 2006 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Sep 04 17:06:45 2006 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4  }
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Variable names%
     3.8 +\isamarkupsection{Names%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
     4.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Mon Sep 04 16:28:36 2006 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Mon Sep 04 17:06:45 2006 +0200
     4.3 @@ -299,47 +299,78 @@
     4.4  \isamarkuptrue%
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -FIXME%
     4.8 +Local results are established by monotonic reasoning from facts
     4.9 +  within a context.  This admits arbitrary combination of theorems,
    4.10 +  e.g.\ using \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or
    4.11 +  equational reasoning.  Unaccounted context manipulations should be
    4.12 +  ruled out, such as raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
    4.13 +  references to free variables or assumptions not present in the proof
    4.14 +  context.
    4.15 +
    4.16 +  \medskip The \isa{prove} operation provides a separate interface
    4.17 +  for structured backwards reasoning under program control, with some
    4.18 +  explicit sanity checks of the result.  The goal context can be
    4.19 +  augmented locally by given fixed variables and assumptions, which
    4.20 +  will be available as local facts during the proof and discharged
    4.21 +  into implications in the result.
    4.22 +
    4.23 +  The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous
    4.24 +  claims within a single goal statement, by using meta-level
    4.25 +  conjunction internally.
    4.26 +
    4.27 +  \medskip The tactical proof of a local claim may be structured
    4.28 +  further by decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
    4.29 +  is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and
    4.30 +  assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
    4.31  \end{isamarkuptext}%
    4.32  \isamarkuptrue%
    4.33  %
    4.34 -\isamarkupsection{Proof states \label{sec:isar-proof-state}%
    4.35 -}
    4.36 -\isamarkuptrue%
    4.37 +\isadelimmlref
    4.38 +%
    4.39 +\endisadelimmlref
    4.40 +%
    4.41 +\isatagmlref
    4.42  %
    4.43  \begin{isamarkuptext}%
    4.44 -FIXME
    4.45 +\begin{mldecls}
    4.46 +  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
    4.47 +\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
    4.48 +  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    4.49 +\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
    4.50 +  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
    4.51 +\verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
    4.52 +\verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic|
    4.53 +  \end{mldecls}
    4.54 +
    4.55 +  \begin{description}
    4.56  
    4.57 -\glossary{Proof state}{The whole configuration of a structured proof,
    4.58 -consisting of a \seeglossary{proof context} and an optional
    4.59 -\seeglossary{structured goal}.  Internally, an Isar proof state is
    4.60 -organized as a stack to accomodate block structure of proof texts.
    4.61 -For historical reasons, a low-level \seeglossary{tactical goal} is
    4.62 -occasionally called ``proof state'' as well.}
    4.63 +  \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of fixed variables \isa{xs} and assumptions
    4.64 +  \isa{As} and applies tactic \isa{tac} to solve it.  The
    4.65 +  latter may depend on the local assumptions being presented as facts.
    4.66 +  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized
    4.67 +  by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}} (the conclusion \isa{C} itself may be a rule statement), turning the quantifier prefix
    4.68 +  into schematic variables, and generalizing implicit type-variables.
    4.69  
    4.70 -\glossary{Structured goal}{FIXME}
    4.71 +  \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
    4.72 +  states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
    4.73 +  subgoals before commencing the actual proof.
    4.74  
    4.75 -\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
    4.76 +  \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
    4.77 +  particular sub-goal, producing an extended context and a reduced
    4.78 +  goal, which needs to be solved by the given tactic.  All schematic
    4.79 +  parameters of the goal are imported into the context as fixed ones,
    4.80 +  which may not be instantiated in the sub-proof.
    4.81 +
    4.82 +  \end{description}%
    4.83  \end{isamarkuptext}%
    4.84  \isamarkuptrue%
    4.85  %
    4.86 -\isamarkupsection{Proof methods%
    4.87 -}
    4.88 -\isamarkuptrue%
    4.89 -%
    4.90 -\begin{isamarkuptext}%
    4.91 -FIXME%
    4.92 -\end{isamarkuptext}%
    4.93 -\isamarkuptrue%
    4.94 +\endisatagmlref
    4.95 +{\isafoldmlref}%
    4.96  %
    4.97 -\isamarkupsection{Attributes%
    4.98 -}
    4.99 -\isamarkuptrue%
   4.100 +\isadelimmlref
   4.101  %
   4.102 -\begin{isamarkuptext}%
   4.103 -FIXME ?!%
   4.104 -\end{isamarkuptext}%
   4.105 -\isamarkuptrue%
   4.106 +\endisadelimmlref
   4.107  %
   4.108  \isadelimtheory
   4.109  %
     5.1 --- a/doc-src/IsarImplementation/Thy/document/session.tex	Mon Sep 04 16:28:36 2006 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/document/session.tex	Mon Sep 04 17:06:45 2006 +0200
     5.3 @@ -8,6 +8,8 @@
     5.4  
     5.5  \input{proof.tex}
     5.6  
     5.7 +\input{isar.tex}
     5.8 +
     5.9  \input{locale.tex}
    5.10  
    5.11  \input{integration.tex}
     6.1 --- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Mon Sep 04 16:28:36 2006 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Mon Sep 04 17:06:45 2006 +0200
     6.3 @@ -163,74 +163,6 @@
     6.4  \end{isamarkuptext}%
     6.5  \isamarkuptrue%
     6.6  %
     6.7 -\isamarkupsection{Programmed proofs%
     6.8 -}
     6.9 -\isamarkuptrue%
    6.10 -%
    6.11 -\begin{isamarkuptext}%
    6.12 -In order to perform a complete tactical proof under program control,
    6.13 -  one needs to set up an initial goal configuration, apply a tactic,
    6.14 -  and finish the result, cf.\ the rules given in
    6.15 -  \secref{sec:tactical-goals}.  Further checks are required to ensure
    6.16 -  that the result is actually an instance of the original claim --
    6.17 -  ill-behaved tactics could have destroyed that information.
    6.18 -
    6.19 -  Several simultaneous claims may be handled within a single goal
    6.20 -  statement by using meta-level conjunction internally.  The whole
    6.21 -  configuration may be considered within a context of
    6.22 -  arbitrary-but-fixed parameters and hypotheses, which will be
    6.23 -  available as local facts during the proof and discharged into
    6.24 -  implications in the result.
    6.25 -
    6.26 -  All of these administrative tasks are packaged into a separate
    6.27 -  operation, such that the user merely needs to provide the statement
    6.28 -  and tactic to be applied.%
    6.29 -\end{isamarkuptext}%
    6.30 -\isamarkuptrue%
    6.31 -%
    6.32 -\isadelimmlref
    6.33 -%
    6.34 -\endisadelimmlref
    6.35 -%
    6.36 -\isatagmlref
    6.37 -%
    6.38 -\begin{isamarkuptext}%
    6.39 -\begin{mldecls}
    6.40 -  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
    6.41 -\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
    6.42 -  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    6.43 -\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
    6.44 -  \indexml{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
    6.45 -\verb|  (thm list -> tactic) -> thm| \\
    6.46 -  \end{mldecls}
    6.47 -
    6.48 -  \begin{description}
    6.49 -
    6.50 -  \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
    6.51 -  and hypotheses \isa{As} and applies tactic \isa{tac} to
    6.52 -  solve it.  The latter may depend on the local assumptions being
    6.53 -  presented as facts.  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
    6.54 -  (the conclusion \isa{C} itself may be a rule statement), turning
    6.55 -  the quantifier prefix into schematic variables, and generalizing
    6.56 -  implicit type-variables.
    6.57 -
    6.58 -  \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
    6.59 -  states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
    6.60 -  subgoals before commencing the actual proof.
    6.61 -
    6.62 -  \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
    6.63 -
    6.64 -  \end{description}%
    6.65 -\end{isamarkuptext}%
    6.66 -\isamarkuptrue%
    6.67 -%
    6.68 -\endisatagmlref
    6.69 -{\isafoldmlref}%
    6.70 -%
    6.71 -\isadelimmlref
    6.72 -%
    6.73 -\endisadelimmlref
    6.74 -%
    6.75  \isadelimtheory
    6.76  %
    6.77  \endisadelimtheory
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/IsarImplementation/Thy/isar.thy	Mon Sep 04 17:06:45 2006 +0200
     7.3 @@ -0,0 +1,36 @@
     7.4 +
     7.5 +(* $Id$ *)
     7.6 +
     7.7 +theory isar imports base begin
     7.8 +
     7.9 +chapter {* Isar proof texts *}
    7.10 +
    7.11 +section {* Proof states \label{sec:isar-proof-state} *}
    7.12 +
    7.13 +text {*
    7.14 +  FIXME
    7.15 +
    7.16 +\glossary{Proof state}{The whole configuration of a structured proof,
    7.17 +consisting of a \seeglossary{proof context} and an optional
    7.18 +\seeglossary{structured goal}.  Internally, an Isar proof state is
    7.19 +organized as a stack to accomodate block structure of proof texts.
    7.20 +For historical reasons, a low-level \seeglossary{tactical goal} is
    7.21 +occasionally called ``proof state'' as well.}
    7.22 +
    7.23 +\glossary{Structured goal}{FIXME}
    7.24 +
    7.25 +\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
    7.26 +
    7.27 +
    7.28 +*}
    7.29 +
    7.30 +section {* Proof methods *}
    7.31 +
    7.32 +text FIXME
    7.33 +
    7.34 +section {* Attributes *}
    7.35 +
    7.36 +text "FIXME ?!"
    7.37 +
    7.38 +
    7.39 +end
     8.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Mon Sep 04 16:28:36 2006 +0200
     8.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Sep 04 17:06:45 2006 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  
     8.5  chapter {* Primitive logic \label{ch:logic} *}
     8.6  
     8.7 -section {* Variable names *}
     8.8 +section {* Names *}
     8.9  
    8.10  text FIXME
    8.11  
     9.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Mon Sep 04 16:28:36 2006 +0200
     9.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Mon Sep 04 17:06:45 2006 +0200
     9.3 @@ -263,34 +263,67 @@
     9.4  
     9.5  section {* Conclusions *}
     9.6  
     9.7 -text FIXME
     9.8 -
     9.9 -
    9.10 -section {* Proof states \label{sec:isar-proof-state} *}
    9.11 -
    9.12  text {*
    9.13 -  FIXME
    9.14 +  Local results are established by monotonic reasoning from facts
    9.15 +  within a context.  This admits arbitrary combination of theorems,
    9.16 +  e.g.\ using @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or
    9.17 +  equational reasoning.  Unaccounted context manipulations should be
    9.18 +  ruled out, such as raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
    9.19 +  references to free variables or assumptions not present in the proof
    9.20 +  context.
    9.21  
    9.22 -\glossary{Proof state}{The whole configuration of a structured proof,
    9.23 -consisting of a \seeglossary{proof context} and an optional
    9.24 -\seeglossary{structured goal}.  Internally, an Isar proof state is
    9.25 -organized as a stack to accomodate block structure of proof texts.
    9.26 -For historical reasons, a low-level \seeglossary{tactical goal} is
    9.27 -occasionally called ``proof state'' as well.}
    9.28 +  \medskip The @{text "prove"} operation provides a separate interface
    9.29 +  for structured backwards reasoning under program control, with some
    9.30 +  explicit sanity checks of the result.  The goal context can be
    9.31 +  augmented locally by given fixed variables and assumptions, which
    9.32 +  will be available as local facts during the proof and discharged
    9.33 +  into implications in the result.
    9.34  
    9.35 -\glossary{Structured goal}{FIXME}
    9.36 +  The @{text "prove_multi"} operation handles several simultaneous
    9.37 +  claims within a single goal statement, by using meta-level
    9.38 +  conjunction internally.
    9.39  
    9.40 -\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}
    9.41 -
    9.42 -
    9.43 +  \medskip The tactical proof of a local claim may be structured
    9.44 +  further by decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"}
    9.45 +  is turned into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and
    9.46 +  assuming @{text "A(x)"}.
    9.47  *}
    9.48  
    9.49 -section {* Proof methods *}
    9.50 +text %mlref {*
    9.51 +  \begin{mldecls}
    9.52 +  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
    9.53 +  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
    9.54 +  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
    9.55 +  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
    9.56 +  @{index_ML SUBPROOF:
    9.57 +  "({context: Proof.context, schematics: ctyp list * cterm list,
    9.58 +    params: cterm list, asms: cterm list, concl: cterm,
    9.59 +    prems: thm list} -> tactic) -> Proof.context -> int -> tactic"}
    9.60 +  \end{mldecls}
    9.61  
    9.62 -text FIXME
    9.63 +  \begin{description}
    9.64  
    9.65 -section {* Attributes *}
    9.66 +  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
    9.67 +  "C"} in the context of fixed variables @{text "xs"} and assumptions
    9.68 +  @{text "As"} and applies tactic @{text "tac"} to solve it.  The
    9.69 +  latter may depend on the local assumptions being presented as facts.
    9.70 +  The result is essentially @{text "\<And>xs. As \<Longrightarrow> C"}, but is normalized
    9.71 +  by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"} (the conclusion @{text
    9.72 +  "C"} itself may be a rule statement), turning the quantifier prefix
    9.73 +  into schematic variables, and generalizing implicit type-variables.
    9.74  
    9.75 -text "FIXME ?!"
    9.76 +  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
    9.77 +  states several conclusions simultaneously.  @{ML
    9.78 +  Tactic.conjunction_tac} may be used to split these into individual
    9.79 +  subgoals before commencing the actual proof.
    9.80 +
    9.81 +  \item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
    9.82 +  particular sub-goal, producing an extended context and a reduced
    9.83 +  goal, which needs to be solved by the given tactic.  All schematic
    9.84 +  parameters of the goal are imported into the context as fixed ones,
    9.85 +  which may not be instantiated in the sub-proof.
    9.86 +
    9.87 +  \end{description}
    9.88 +*}
    9.89  
    9.90  end
    10.1 --- a/doc-src/IsarImplementation/Thy/tactic.thy	Mon Sep 04 16:28:36 2006 +0200
    10.2 +++ b/doc-src/IsarImplementation/Thy/tactic.thy	Mon Sep 04 17:06:45 2006 +0200
    10.3 @@ -134,61 +134,5 @@
    10.4  
    10.5  *}
    10.6  
    10.7 -section {* Programmed proofs *}
    10.8 -
    10.9 -text {*
   10.10 -  In order to perform a complete tactical proof under program control,
   10.11 -  one needs to set up an initial goal configuration, apply a tactic,
   10.12 -  and finish the result, cf.\ the rules given in
   10.13 -  \secref{sec:tactical-goals}.  Further checks are required to ensure
   10.14 -  that the result is actually an instance of the original claim --
   10.15 -  ill-behaved tactics could have destroyed that information.
   10.16 -
   10.17 -  Several simultaneous claims may be handled within a single goal
   10.18 -  statement by using meta-level conjunction internally.  The whole
   10.19 -  configuration may be considered within a context of
   10.20 -  arbitrary-but-fixed parameters and hypotheses, which will be
   10.21 -  available as local facts during the proof and discharged into
   10.22 -  implications in the result.
   10.23 -
   10.24 -  All of these administrative tasks are packaged into a separate
   10.25 -  operation, such that the user merely needs to provide the statement
   10.26 -  and tactic to be applied.
   10.27 -*}
   10.28 -
   10.29 -text %mlref {*
   10.30 -  \begin{mldecls}
   10.31 -  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   10.32 -  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
   10.33 -  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
   10.34 -  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
   10.35 -  @{index_ML Goal.prove_global: "theory -> string list -> term list -> term ->
   10.36 -  (thm list -> tactic) -> thm"} \\
   10.37 -  \end{mldecls}
   10.38 -
   10.39 -  \begin{description}
   10.40 -
   10.41 -  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
   10.42 -  "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
   10.43 -  and hypotheses @{text "As"} and applies tactic @{text "tac"} to
   10.44 -  solve it.  The latter may depend on the local assumptions being
   10.45 -  presented as facts.  The result is essentially @{text "\<And>xs. As \<Longrightarrow>
   10.46 -  C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
   10.47 -  (the conclusion @{text "C"} itself may be a rule statement), turning
   10.48 -  the quantifier prefix into schematic variables, and generalizing
   10.49 -  implicit type-variables.
   10.50 -
   10.51 -  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
   10.52 -  states several conclusions simultaneously.  @{ML
   10.53 -  Tactic.conjunction_tac} may be used to split these into individual
   10.54 -  subgoals before commencing the actual proof.
   10.55 -
   10.56 -  \item @{ML Goal.prove_global} is a degraded version of @{ML
   10.57 -  Goal.prove} for theory level goals; it includes a global @{ML
   10.58 -  Drule.standard} for the result.
   10.59 -
   10.60 -  \end{description}
   10.61 -*}
   10.62 -
   10.63  end
   10.64  
    11.1 --- a/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 16:28:36 2006 +0200
    11.2 +++ b/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 17:06:45 2006 +0200
    11.3 @@ -65,6 +65,7 @@
    11.4  \input{Thy/document/logic.tex}
    11.5  \input{Thy/document/tactic.tex}
    11.6  \input{Thy/document/proof.tex}
    11.7 +\input{Thy/document/isar.tex}
    11.8  \input{Thy/document/locale.tex}
    11.9  \input{Thy/document/integration.tex}
   11.10