22 term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory |
22 term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory |
23 val typedef: (bool * string) * (bstring * string list * mixfix) * string |
23 val typedef: (bool * string) * (bstring * string list * mixfix) * string |
24 * (string * string) option -> theory -> Proof.state |
24 * (string * string) option -> theory -> Proof.state |
25 val typedef_i: (bool * string) * (bstring * string list * mixfix) * term |
25 val typedef_i: (bool * string) * (bstring * string list * mixfix) * term |
26 * (string * string) option -> theory -> Proof.state |
26 * (string * string) option -> theory -> Proof.state |
27 val setup: theory -> theory |
|
28 end; |
27 end; |
29 |
28 |
30 structure TypedefPackage: TYPEDEF_PACKAGE = |
29 structure TypedefPackage: TYPEDEF_PACKAGE = |
31 struct |
30 struct |
32 |
31 |
75 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
74 type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
76 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
75 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, |
77 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
76 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; |
78 |
77 |
79 structure TypedefData = TheoryDataFun |
78 structure TypedefData = TheoryDataFun |
80 (struct |
79 ( |
81 val name = "HOL/typedef"; |
|
82 type T = info Symtab.table; |
80 type T = info Symtab.table; |
83 val empty = Symtab.empty; |
81 val empty = Symtab.empty; |
84 val copy = I; |
82 val copy = I; |
85 val extend = I; |
83 val extend = I; |
86 fun merge _ tabs : T = Symtab.merge (K true) tabs; |
84 fun merge _ tabs : T = Symtab.merge (K true) tabs; |
87 fun print _ _ = (); |
85 ); |
88 end); |
|
89 |
86 |
90 val get_info = Symtab.lookup o TypedefData.get; |
87 val get_info = Symtab.lookup o TypedefData.get; |
91 fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
88 fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
92 |
89 |
93 |
90 |