equal
deleted
inserted
replaced
22 |
22 |
23 text %mlref {* |
23 text %mlref {* |
24 \begin{mldecls} |
24 \begin{mldecls} |
25 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
25 @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\ |
26 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
26 @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
27 @{index_ML Code.add_eqnl: "string * (thm * bool) list Lazy.T -> theory -> theory"} \\ |
27 @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\ |
28 @{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\ |
28 @{index_ML Code.map_pre: "(simpset -> simpset) -> theory -> theory"} \\ |
29 @{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\ |
29 @{index_ML Code.map_post: "(simpset -> simpset) -> theory -> theory"} \\ |
30 @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) |
30 @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option) |
31 -> theory -> theory"} \\ |
31 -> theory -> theory"} \\ |
32 @{index_ML Code.del_functrans: "string -> theory -> theory"} \\ |
32 @{index_ML Code.del_functrans: "string -> theory -> theory"} \\ |
33 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
33 @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
34 @{index_ML Code.get_datatype: "theory -> string |
34 @{index_ML Code.get_datatype: "theory -> string |
78 |
78 |
79 text %mlref {* |
79 text %mlref {* |
80 \begin{mldecls} |
80 \begin{mldecls} |
81 @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ |
81 @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ |
82 @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\ |
82 @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\ |
83 @{index_ML Code_Unit.rewrite_eqn: "MetaSimplifier.simpset -> thm -> thm"} \\ |
83 @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\ |
84 \end{mldecls} |
84 \end{mldecls} |
85 |
85 |
86 \begin{description} |
86 \begin{description} |
87 |
87 |
88 \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} |
88 \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} |