equal
deleted
inserted
replaced
4 Partial function definitions based on least fixed points in ccpos. |
4 Partial function definitions based on least fixed points in ccpos. |
5 *) |
5 *) |
6 |
6 |
7 signature PARTIAL_FUNCTION = |
7 signature PARTIAL_FUNCTION = |
8 sig |
8 sig |
9 val init: string -> term -> term -> thm -> thm -> thm option -> declaration |
9 val init: string -> term -> term -> thm -> thm -> thm option -> Morphism.declaration_fn |
10 val mono_tac: Proof.context -> int -> tactic |
10 val mono_tac: Proof.context -> int -> tactic |
11 val add_partial_function: string -> (binding * typ option * mixfix) list -> |
11 val add_partial_function: string -> (binding * typ option * mixfix) list -> |
12 Attrib.binding * term -> local_theory -> (term * thm) * local_theory |
12 Attrib.binding * term -> local_theory -> (term * thm) * local_theory |
13 val add_partial_function_cmd: string -> (binding * string option * mixfix) list -> |
13 val add_partial_function_cmd: string -> (binding * string option * mixfix) list -> |
14 Attrib.binding * string -> local_theory -> (term * thm) * local_theory |
14 Attrib.binding * string -> local_theory -> (term * thm) * local_theory |