more uniform treatment of options and attributes, preferring formal markup over old-style LaTeX macros;

--- a/doc-src/IsarRef/Thy/Proof.thy	Mon Jun 07 18:09:18 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Jun 07 19:21:00 2010 +0200
@@ -1320,9 +1320,9 @@
   of premises of the case rule; within each premise, the \emph{prefix}
   of variables is instantiated.  In most situations, only a single
   term needs to be specified; this refers to the first variable of the
-  last premise (it is usually the same for all cases).
-  The \texttt{no\_simp} option can be used to disable pre-simplification
-  of cases (see the description of @{method induct} below for details).
+  last premise (it is usually the same for all cases).  The @{text
+  "(no_simp)"} option can be used to disable pre-simplification of
+  cases (see the description of @{method induct} below for details).
 
   \item @{method induct}~@{text "insts R"} is analogous to the
   @{method cases} method, but refers to induction rules, which are
@@ -1344,28 +1344,28 @@
   present in the induction rule.  This enables the writer to specify
   only induction variables, or both predicates and variables, for
   example.
-  
+
   Instantiations may be definitional: equations @{text "x \<equiv> t"}
   introduce local definitions, which are inserted into the claim and
   discharged after applying the induction rule.  Equalities reappear
   in the inductive cases, but have been transformed according to the
   induction principle being involved here.  In order to achieve
   practically useful induction hypotheses, some variables occurring in
-  @{text t} need to be fixed (see below).
-  Instantiations of the form @{text t}, where @{text t} is not a variable,
-  are taken as a shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is
-  a fresh variable. If this is not intended, @{text t} has to be enclosed in
-  parentheses.
-  By default, the equalities generated by definitional instantiations
-  are pre-simplified using a specific set of rules, usually consisting
-  of distinctness and injectivity theorems for datatypes. This pre-simplification
-  may cause some of the parameters of an inductive case to disappear,
-  or may even completely delete some of the inductive cases, if one of
-  the equalities occurring in their premises can be simplified to @{text False}.
-  The \texttt{no\_simp} option can be used to disable pre-simplification.
-  Additional rules to be used in pre-simplification can be declared using the
-  \texttt{induct\_simp} attribute.
-  
+  @{text t} need to be fixed (see below).  Instantiations of the form
+  @{text t}, where @{text t} is not a variable, are taken as a
+  shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
+  variable. If this is not intended, @{text t} has to be enclosed in
+  parentheses.  By default, the equalities generated by definitional
+  instantiations are pre-simplified using a specific set of rules,
+  usually consisting of distinctness and injectivity theorems for
+  datatypes. This pre-simplification may cause some of the parameters
+  of an inductive case to disappear, or may even completely delete
+  some of the inductive cases, if one of the equalities occurring in
+  their premises can be simplified to @{text False}.  The @{text
+  "(no_simp)"} option can be used to disable pre-simplification.
+  Additional rules to be used in pre-simplification can be declared
+  using the @{attribute_def induct_simp} attribute.
+
   The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
   specification generalizes variables @{text "x\<^sub>1, \<dots>,
   x\<^sub>m"} of the original goal before applying induction.  Thus

--- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Jun 07 18:09:18 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Jun 07 19:21:00 2010 +0200
@@ -1317,9 +1317,8 @@
   of premises of the case rule; within each premise, the \emph{prefix}
   of variables is instantiated.  In most situations, only a single
   term needs to be specified; this refers to the first variable of the
-  last premise (it is usually the same for all cases).
-  The \texttt{no\_simp} option can be used to disable pre-simplification
-  of cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
+  last premise (it is usually the same for all cases).  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of
+  cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
 
   \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
   \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
@@ -1341,28 +1340,27 @@
   present in the induction rule.  This enables the writer to specify
   only induction variables, or both predicates and variables, for
   example.
-  
+
   Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
   introduce local definitions, which are inserted into the claim and
   discharged after applying the induction rule.  Equalities reappear
   in the inductive cases, but have been transformed according to the
   induction principle being involved here.  In order to achieve
   practically useful induction hypotheses, some variables occurring in
-  \isa{t} need to be fixed (see below).
-  Instantiations of the form \isa{t}, where \isa{t} is not a variable,
-  are taken as a shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is
-  a fresh variable. If this is not intended, \isa{t} has to be enclosed in
-  parentheses.
-  By default, the equalities generated by definitional instantiations
-  are pre-simplified using a specific set of rules, usually consisting
-  of distinctness and injectivity theorems for datatypes. This pre-simplification
-  may cause some of the parameters of an inductive case to disappear,
-  or may even completely delete some of the inductive cases, if one of
-  the equalities occurring in their premises can be simplified to \isa{False}.
-  The \texttt{no\_simp} option can be used to disable pre-simplification.
-  Additional rules to be used in pre-simplification can be declared using the
-  \texttt{induct\_simp} attribute.
-  
+  \isa{t} need to be fixed (see below).  Instantiations of the form
+  \isa{t}, where \isa{t} is not a variable, are taken as a
+  shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
+  variable. If this is not intended, \isa{t} has to be enclosed in
+  parentheses.  By default, the equalities generated by definitional
+  instantiations are pre-simplified using a specific set of rules,
+  usually consisting of distinctness and injectivity theorems for
+  datatypes. This pre-simplification may cause some of the parameters
+  of an inductive case to disappear, or may even completely delete
+  some of the inductive cases, if one of the equalities occurring in
+  their premises can be simplified to \isa{False}.  The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification.
+  Additional rules to be used in pre-simplification can be declared
+  using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
+
   The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
   specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction.  Thus
   induction hypotheses may become sufficiently general to get the