doc-src/IsarRef/Thy/Generic.thy

 
   \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts
   into all goals of the proof state.  Note that current facts
   indicated for forward chaining are ignored.
 
-  \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1
-  \<dots> a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the
-  basic @{method rule} method (see \secref{sec:pure-meth-att}), but
-  apply rules by elim-resolution, destruct-resolution, and
-  forward-resolution, respectively \cite{isabelle-ref}.  The optional
-  natural number argument (default 0) specifies additional assumption
-  steps to be performed here.
+  \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method
+  drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text
+  "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule}
+  method (see \secref{sec:pure-meth-att}), but apply rules by
+  elim-resolution, destruct-resolution, and forward-resolution,
+  respectively \cite{isabelle-implementation}.  The optional natural
+  number argument (default 0) specifies additional assumption steps to
+  be performed here.
 
   Note that these methods are improper ones, mainly serving for
   experimentation and tactic script emulation.  Different modes of
   basic rule application are usually expressed in Isar at the proof
   language level, rather than via implicit proof state manipulations.

   compose rules by resolution.  @{attribute THEN} resolves with the
   first premise of @{text a} (an alternative position may be also
   specified); the @{attribute COMP} version skips the automatic
   lifting process that is normally intended (cf.\ @{ML [source=false]
   "op RS"} and @{ML [source=false] "op COMP"} in
-  \cite[\S5]{isabelle-ref}).
+  \cite{isabelle-implementation}).
   
   \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
   folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
   definitions throughout a rule.
 

 
 \begin{description}
 
   \item @{method rule_tac} etc. do resolution of rules with explicit
   instantiation.  This works the same way as the ML tactics @{ML
-  res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
+  res_inst_tac} etc. (see \cite{isabelle-implementation})
 
   Multiple rules may be only given if there is no instantiation; then
   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
-  \cite[\S3]{isabelle-ref}).
+  \cite{isabelle-implementation}).
 
   \item @{method cut_tac} inserts facts into the proof state as
   assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
-  \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
+  \cite{isabelle-implementation}.  Note that the scope of schematic
   variables is spread over the main goal statement.  Instantiations
   may be given as well, see also ML tactic @{ML cut_inst_tac} in
-  \cite[\S3]{isabelle-ref}.
+  \cite{isabelle-implementation}.
 
   \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
   from a subgoal; note that @{text \<phi>} may contain schematic variables.
-  See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}.
+  See also @{ML thin_tac} in \cite{isabelle-implementation}.
 
   \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
   assumption to a subgoal.  See also @{ML subgoal_tac} and @{ML
-  subgoals_tac} in \cite[\S3]{isabelle-ref}.
+  subgoals_tac} in \cite{isabelle-implementation}.
 
   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   \emph{suffix} of variables.
 
   \item @{method rotate_tac}~@{text n} rotates the assumptions of a
   goal by @{text n} positions: from right to left if @{text n} is
   positive, and from left to right if @{text n} is negative; the
   default value is 1.  See also @{ML rotate_tac} in
-  \cite[\S3]{isabelle-ref}.
+  \cite{isabelle-implementation}.
 
   \item @{method tactic}~@{text "text"} produces a proof method from
   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   environment and the current proof context, the ML code may refer to
   the locally bound values @{ML_text facts}, which indicates any

   \end{description}
 
   By default the Simplifier methods take local assumptions fully into
   account, using equational assumptions in the subsequent
   normalization process, or simplifying assumptions themselves (cf.\
-  @{ML asm_full_simp_tac} in \cite[\S10]{isabelle-ref}).  In
-  structured proofs this is usually quite well behaved in practice:
-  just the local premises of the actual goal are involved, additional
-  facts may be inserted via explicit forward-chaining (via @{command
-  "then"}, @{command "from"}, @{command "using"} etc.).  The full
-  context of premises is only included if the ``@{text "!"}'' (bang)
-  argument is given, which should be used with some care, though.
+  @{ML asm_full_simp_tac} in \cite{isabelle-ref}).  In structured
+  proofs this is usually quite well behaved in practice: just the
+  local premises of the actual goal are involved, additional facts may
+  be inserted via explicit forward-chaining (via @{command "then"},
+  @{command "from"}, @{command "using"} etc.).  The full context of
+  premises is only included if the ``@{text "!"}'' (bang) argument is
+  given, which should be used with some care, though.
 
   Additional Simplifier options may be specified to tune the behavior
   further (mostly for unstructured scripts with many accidental local
   facts): ``@{text "(no_asm)"}'' means assumptions are ignored
   completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means

   \end{rail}
 
   \begin{description}
 
   \item @{method blast} refers to the classical tableau prover (see
-  @{ML blast_tac} in \cite[\S11]{isabelle-ref}).  The optional
-  argument specifies a user-supplied search bound (default 20).
+  @{ML blast_tac} in \cite{isabelle-ref}).  The optional argument
+  specifies a user-supplied search bound (default 20).
 
   \item @{method fast}, @{method slow}, @{method best}, @{method
   safe}, and @{method clarify} refer to the generic classical
   reasoner.  See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML
-  safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for
-  more information.
+  safe_tac}, and @{ML clarify_tac} in \cite{isabelle-ref} for more
+  information.
 
   \end{description}
 
   Any of the above methods support additional modifiers of the context
   of classical rules.  Their semantics is analogous to the attributes

   \item @{method auto}, @{method force}, @{method clarsimp}, @{method
   fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access
   to Isabelle's combined simplification and classical reasoning
   tactics.  These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML
   clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
-  added as wrapper, see \cite[\S11]{isabelle-ref} for more
-  information.  The modifier arguments correspond to those given in
+  added as wrapper, see \cite{isabelle-ref} for more information.  The
+  modifier arguments correspond to those given in
   \secref{sec:simplifier} and \secref{sec:classical}.  Just note that
   the ones related to the Simplifier are prefixed by \railtterm{simp}
   here.
 
   Facts provided by forward chaining are inserted into the goal before