src/Doc/Implementation/Logic.thy

   @{cite "nipkow-prehofer"}.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type class: string} \\
-  @{index_ML_type sort: "class list"} \\
-  @{index_ML_type arity: "string * sort list * sort"} \\
+  @{index_ML_type class = string} \\
+  @{index_ML_type sort = "class list"} \\
+  @{index_ML_type arity = "string * sort list * sort"} \\
   @{index_ML_type typ} \\
   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   \end{mldecls}
   \begin{mldecls}

 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type term} \\
-  @{index_ML_op "aconv": "term * term -> bool"} \\
+  @{index_ML_infix "aconv": "term * term -> bool"} \\
   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   \end{mldecls}

   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>term\<close> represents de-Bruijn terms, with comments in
   abstractions, and explicitly named free variables and constants; this is a
   datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML
-  Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_op "$"}.
+  Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_infix "$"}.
 
   \<^descr> \<open>t\<close>~\<^ML_text>\<open>aconv\<close>~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the
   basic equality relation on type \<^ML_type>\<open>term\<close>; raw datatype equality
   should only be used for operations related to parsing or printing!
 

   %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
-  @{index_ML_op "RS": "thm * thm -> thm"} \\
-
-  @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
-  @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
-
-  @{index_ML_op "MRS": "thm list * thm -> thm"} \\
-  @{index_ML_op "OF": "thm * thm list -> thm"} \\
+  @{index_ML_infix "RSN": "thm * (int * thm) -> thm"} \\
+  @{index_ML_infix "RS": "thm * thm -> thm"} \\
+
+  @{index_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\
+  @{index_ML_infix "RL": "thm list * thm list -> thm list"} \\
+
+  @{index_ML_infix "MRS": "thm list * thm -> thm"} \\
+  @{index_ML_infix "OF": "thm * thm list -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the
   \<open>i\<close>-th premise of \<open>rule\<^sub>2\<close>, according to the @{inference resolution}
   principle explained above. Unless there is precisely one resolvent it raises

   @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
-  constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
-  @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
+  constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_infix "%"},
+  @{index_ML_infix "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
   Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
   above. %FIXME PClass (!?)
 
   \<^descr> Type \<^ML_type>\<open>proof_body\<close> represents the nested proof information of a
   named theorem, consisting of a digest of oracles and named theorem over some