equal
deleted
inserted
replaced
207 \begin{mldecls} |
207 \begin{mldecls} |
208 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
208 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
209 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
209 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
210 @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ |
210 @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ |
211 @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ |
211 @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\ |
212 @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) |
212 @{index_ML Code_Preproc.add_functrans: " |
213 -> theory -> theory"} \\ |
213 string * (theory -> (thm * bool) list -> (thm * bool) list option) |
|
214 -> theory -> theory"} \\ |
214 @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ |
215 @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ |
215 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
216 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
216 @{index_ML Code.get_type: "theory -> string |
217 @{index_ML Code.get_type: "theory -> string |
217 -> (string * sort) list * ((string * string list) * typ list) list"} \\ |
218 -> (string * sort) list * ((string * string list) * typ list) list"} \\ |
218 @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} |
219 @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} |