18 term list * term list -> local_theory -> (term * thm) * local_theory |
18 term list * term list -> local_theory -> (term * thm) * local_theory |
19 val background_declaration: declaration -> local_theory -> local_theory |
19 val background_declaration: declaration -> local_theory -> local_theory |
20 val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory |
20 val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory |
21 |
21 |
22 (*nested local theories primitives*) |
22 (*nested local theories primitives*) |
23 val standard_facts: local_theory -> Proof.context -> |
23 val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list |
24 (Attrib.binding * Attrib.thms) list -> (Attrib.binding * Attrib.thms) list |
24 val standard_notes: (int * int -> bool) -> string -> Attrib.fact list -> |
25 val standard_notes: (int * int -> bool) -> string -> (Attrib.binding * Attrib.thms) list -> |
|
26 local_theory -> local_theory |
25 local_theory -> local_theory |
27 val standard_declaration: (int * int -> bool) -> |
26 val standard_declaration: (int * int -> bool) -> |
28 (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
27 (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory |
29 val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> |
28 val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> |
30 local_theory -> local_theory |
29 local_theory -> local_theory |
33 val define: (((binding * typ) * mixfix) * (binding * term) -> |
32 val define: (((binding * typ) * mixfix) * (binding * term) -> |
34 term list * term list -> local_theory -> (term * thm) * local_theory) -> |
33 term list * term list -> local_theory -> (term * thm) * local_theory) -> |
35 bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
34 bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> |
36 (term * (string * thm)) * local_theory |
35 (term * (string * thm)) * local_theory |
37 val notes: |
36 val notes: |
38 (string -> (Attrib.binding * Attrib.thms) list -> |
37 (string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) -> |
39 (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory) -> |
38 string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory |
40 string -> (Attrib.binding * Attrib.thms) list -> local_theory -> |
|
41 (string * thm list) list * local_theory |
|
42 val abbrev: (Syntax.mode -> binding * mixfix -> term -> |
39 val abbrev: (Syntax.mode -> binding * mixfix -> term -> |
43 term list * term list -> local_theory -> local_theory) -> |
40 term list * term list -> local_theory -> local_theory) -> |
44 Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory |
41 Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory |
45 |
42 |
46 (*theory target primitives*) |
43 (*theory target primitives*) |
47 val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
44 val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
48 term list * term list -> local_theory -> (term * thm) * local_theory |
45 term list * term list -> local_theory -> (term * thm) * local_theory |
49 val theory_target_notes: string -> (Attrib.binding * Attrib.thms) list -> |
46 val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list -> |
50 (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory |
47 local_theory -> local_theory |
51 val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> |
48 val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> |
52 local_theory -> local_theory |
49 local_theory -> local_theory |
53 |
50 |
54 (*theory target operations*) |
51 (*theory target operations*) |
55 val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> |
52 val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> |
57 val theory_declaration: declaration -> local_theory -> local_theory |
54 val theory_declaration: declaration -> local_theory -> local_theory |
58 val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
55 val theory_registration: string * morphism -> (morphism * bool) option -> morphism -> |
59 local_theory -> local_theory |
56 local_theory -> local_theory |
60 |
57 |
61 (*locale target primitives*) |
58 (*locale target primitives*) |
62 val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list -> |
59 val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> |
63 (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory |
60 local_theory -> local_theory |
64 val locale_target_abbrev: string -> Syntax.mode -> |
61 val locale_target_abbrev: string -> Syntax.mode -> |
65 (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory |
62 (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory |
66 val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory |
63 val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory |
67 val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> |
64 val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> |
68 (binding * mixfix) * term -> local_theory -> local_theory |
65 (binding * mixfix) * term -> local_theory -> local_theory |