src/Doc/Implementation/Eq.thy

   \<open>\<beta>\<eta>\<close>-conversion) and lifting of \<open>\<And>/\<Longrightarrow>\<close> contexts.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Thm.reflexive: "cterm -> thm"} \\
-  @{index_ML Thm.symmetric: "thm -> thm"} \\
-  @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
-  @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
-  @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
-  @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
-  @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
+  @{define_ML Thm.reflexive: "cterm -> thm"} \\
+  @{define_ML Thm.symmetric: "thm -> thm"} \\
+  @{define_ML Thm.transitive: "thm -> thm -> thm"} \\
+  @{define_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
+  @{define_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
+  @{define_ML Thm.equal_intr: "thm -> thm -> thm"} \\
+  @{define_ML Thm.equal_elim: "thm -> thm -> thm"} \\
   \end{mldecls}
 
   See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
   rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
   conversion is implicit due to the representation of terms with de-Bruijn

   differently, see @{cite \<open>\S9.3\<close> "isabelle-isar-ref"}.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_structure Conv} \\
-  @{index_ML_type conv} \\
-  @{index_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
+  @{define_ML_structure Conv} \\
+  @{define_ML_type conv} \\
+  @{define_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\
   \end{mldecls}
 
   \<^descr> \<^ML_structure>\<open>Conv\<close> is a library of combinators to build conversions,
   over type \<^ML_type>\<open>conv\<close> (see also \<^file>\<open>~~/src/Pure/conv.ML\<close>). This is one
   of the few Isabelle/ML modules that are usually used with \<^verbatim>\<open>open\<close>: finding

   definitions of the form \<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> u\<close>, but is slightly more general than
   that. \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
-  @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
-  @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
+  @{define_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{define_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\
+  @{define_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\
+  @{define_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>rewrite_rule\<close>~\<open>ctxt rules thm\<close> rewrites the whole theorem by the
   given rules.