author | wenzelm |
Sat, 06 Mar 2010 17:32:45 +0100 | |
changeset 35615 | 61bb9f8af129 |
parent 35430 | df2862dc23a8 |
child 35625 | 9c818cab0dd0 |
permissions | -rw-r--r-- |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
1 |
(* Title: HOL/Tools/typedef.ML |
16458 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
4866 | 3 |
|
21352 | 4 |
Gordon/HOL-style type definitions: create a new syntactic type |
5 |
represented by a non-empty subset. |
|
4866 | 6 |
*) |
7 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
8 |
signature TYPEDEF = |
4866 | 9 |
sig |
19705 | 10 |
type info = |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
11 |
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
12 |
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
13 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
14 |
Rep_induct: thm, Abs_induct: thm} |
30345 | 15 |
val add_typedef: bool -> binding option -> binding * string list * mixfix -> |
16 |
term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory |
|
35202
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
17 |
val typedef: (bool * binding) * (binding * string list * mixfix) * term * |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
18 |
(binding * binding) option -> theory -> Proof.state |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
19 |
val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string * |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
20 |
(binding * binding) option -> theory -> Proof.state |
31735 | 21 |
val get_info: theory -> string -> info option |
35134 | 22 |
val the_info: theory -> string -> info |
25513 | 23 |
val interpretation: (string -> theory -> theory) -> theory -> theory |
25535 | 24 |
val setup: theory -> theory |
4866 | 25 |
end; |
26 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
27 |
structure Typedef: TYPEDEF = |
4866 | 28 |
struct |
29 |
||
17922 | 30 |
(** type definitions **) |
31 |
||
32 |
(* theory data *) |
|
15259 | 33 |
|
19705 | 34 |
type info = |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
35 |
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
36 |
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
37 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
38 |
Rep_induct: thm, Abs_induct: thm}; |
19459 | 39 |
|
33522 | 40 |
structure TypedefData = Theory_Data |
22846 | 41 |
( |
19705 | 42 |
type T = info Symtab.table; |
15259 | 43 |
val empty = Symtab.empty; |
16458 | 44 |
val extend = I; |
33522 | 45 |
fun merge data = Symtab.merge (K true) data; |
22846 | 46 |
); |
15259 | 47 |
|
19705 | 48 |
val get_info = Symtab.lookup o TypedefData.get; |
35134 | 49 |
|
50 |
fun the_info thy name = |
|
51 |
(case get_info thy name of |
|
52 |
SOME info => info |
|
53 |
| NONE => error ("Unknown typedef " ^ quote name)); |
|
54 |
||
19705 | 55 |
fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
15259 | 56 |
|
57 |
||
6383 | 58 |
(* prepare_typedef *) |
59 |
||
21352 | 60 |
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
61 |
||
33314 | 62 |
structure Typedef_Interpretation = Interpretation(type T = string val eq = op =); |
63 |
val interpretation = Typedef_Interpretation.interpretation; |
|
25535 | 64 |
|
35129 | 65 |
fun prepare_typedef prep_term def name (tname, vs, mx) raw_set opt_morphs thy = |
4866 | 66 |
let |
11608 | 67 |
val _ = Theory.requires thy "Typedef" "typedefs"; |
21352 | 68 |
val ctxt = ProofContext.init thy; |
30345 | 69 |
|
70 |
val full = Sign.full_name thy; |
|
71 |
val full_name = full name; |
|
72 |
val bname = Binding.name_of name; |
|
4866 | 73 |
|
74 |
(*rhs*) |
|
21352 | 75 |
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
76 |
val setT = Term.fastype_of set; |
|
17280 | 77 |
val rhs_tfrees = Term.add_tfrees set []; |
78 |
val rhs_tfreesT = Term.add_tfreesT setT []; |
|
4866 | 79 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
24920 | 80 |
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
4866 | 81 |
|
82 |
(*lhs*) |
|
17280 | 83 |
val defS = Sign.defaultS thy; |
19473 | 84 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
17280 | 85 |
val args_setT = lhs_tfrees |
86 |
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT)) |
|
87 |
|> map TFree; |
|
88 |
||
10280 | 89 |
val full_tname = full tname; |
90 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
|
4866 | 91 |
|
30345 | 92 |
val (Rep_name, Abs_name) = |
93 |
(case opt_morphs of |
|
94 |
NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
|
95 |
| SOME morphs => morphs); |
|
19391 | 96 |
val setT' = map Term.itselfT args_setT ---> setT; |
17280 | 97 |
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); |
10280 | 98 |
val RepC = Const (full Rep_name, newT --> oldT); |
99 |
val AbsC = Const (full Abs_name, oldT --> newT); |
|
100 |
||
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
101 |
(*inhabitance*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
102 |
fun mk_inhabited A = |
29054
6f61794f1ff7
logically separate typedef axiomatization from constant definition
krauss
parents:
29053
diff
changeset
|
103 |
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
104 |
val set' = if def then setC else set; |
29062 | 105 |
val goal' = mk_inhabited set'; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
106 |
val goal = mk_inhabited set; |
30345 | 107 |
val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT)); |
4866 | 108 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
109 |
(*axiomatization*) |
30345 | 110 |
val typedef_name = Binding.prefix_name "type_definition_" name; |
10280 | 111 |
val typedefC = |
29056 | 112 |
Const (@{const_name type_definition}, |
113 |
(newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
114 |
val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
30345 | 115 |
val typedef_deps = Term.add_consts set' []; |
4866 | 116 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
117 |
(*set definition*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
118 |
fun add_def theory = |
29056 | 119 |
if def then |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
120 |
theory |
35430
df2862dc23a8
adapted to authentic syntax -- actual types are verbatim;
wenzelm
parents:
35351
diff
changeset
|
121 |
|> Sign.add_consts_i [(name, setT', NoSyn)] |
35238 | 122 |
|> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])] |
19705 | 123 |
|-> (fn [th] => pair (SOME th)) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
124 |
else (NONE, theory); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
125 |
fun contract_def NONE th = th |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
126 |
| contract_def (SOME def_eq) th = |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
127 |
let |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
128 |
val cert = Thm.cterm_of (Thm.theory_of_thm def_eq); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
129 |
val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal'); |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33522
diff
changeset
|
130 |
in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end; |
18358 | 131 |
|
29056 | 132 |
fun typedef_result inhabited = |
35129 | 133 |
ObjectLogic.typedecl (tname, vs, mx) |
25458
ba8f5e4fa336
separated typedecl module, providing typedecl command with interpretation
haftmann
parents:
24926
diff
changeset
|
134 |
#> snd |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
135 |
#> Sign.add_consts_i |
6383 | 136 |
[(Rep_name, newT --> oldT, NoSyn), |
29053 | 137 |
(Abs_name, oldT --> newT, NoSyn)] |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
138 |
#> add_def |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
139 |
#-> (fn set_def => |
30345 | 140 |
PureThy.add_axioms [((typedef_name, typedef_prop), |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
141 |
[Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])] |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
142 |
##>> pair set_def) |
21352 | 143 |
##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
144 |
##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
145 |
#-> (fn ([type_definition], set_def) => fn thy1 => |
11822 | 146 |
let |
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
33522
diff
changeset
|
147 |
fun make th = Drule.export_without_context (th OF [type_definition]); |
18377 | 148 |
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
19705 | 149 |
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
150 |
thy1 |
|
30345 | 151 |
|> Sign.add_path (Binding.name_of name) |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset
|
152 |
|> PureThy.add_thms |
30345 | 153 |
[((Rep_name, make @{thm type_definition.Rep}), []), |
154 |
((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []), |
|
155 |
((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []), |
|
156 |
((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []), |
|
157 |
((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []), |
|
158 |
((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}), |
|
33368 | 159 |
[Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]), |
30345 | 160 |
((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}), |
33368 | 161 |
[Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]), |
30345 | 162 |
((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}), |
33368 | 163 |
[Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), |
30345 | 164 |
((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}), |
33368 | 165 |
[Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])] |
35202
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
166 |
||> Sign.restore_naming thy1; |
19705 | 167 |
val info = {rep_type = oldT, abs_type = newT, |
168 |
Rep_name = full Rep_name, Abs_name = full Abs_name, |
|
28848 | 169 |
inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
19705 | 170 |
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
171 |
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, |
|
11822 | 172 |
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; |
25535 | 173 |
in |
174 |
thy2 |
|
175 |
|> put_info full_tname info |
|
33314 | 176 |
|> Typedef_Interpretation.data full_tname |
25535 | 177 |
|> pair (full_tname, info) |
178 |
end); |
|
6383 | 179 |
|
29056 | 180 |
|
4866 | 181 |
(* errors *) |
182 |
||
183 |
fun show_names pairs = commas_quote (map fst pairs); |
|
184 |
||
185 |
val illegal_vars = |
|
29264 | 186 |
if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then [] |
4866 | 187 |
else ["Illegal schematic variable(s) on rhs"]; |
188 |
||
189 |
val dup_lhs_tfrees = |
|
18964 | 190 |
(case duplicates (op =) lhs_tfrees of [] => [] |
4866 | 191 |
| dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
192 |
||
193 |
val extra_rhs_tfrees = |
|
17280 | 194 |
(case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] |
4866 | 195 |
| extras => ["Extra type variables on rhs: " ^ show_names extras]); |
196 |
||
197 |
val illegal_frees = |
|
29264 | 198 |
(case Term.add_frees set [] of [] => [] |
199 |
| xs => ["Illegal variables on rhs: " ^ show_names xs]); |
|
4866 | 200 |
|
201 |
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; |
|
11426
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
202 |
val _ = if null errs then () else error (cat_lines errs); |
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
203 |
|
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
204 |
(*test theory errors now!*) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
205 |
val test_thy = Theory.copy thy; |
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32966
diff
changeset
|
206 |
val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy; |
11426
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
207 |
|
29062 | 208 |
in (set, goal, goal_pat, typedef_result) end |
30345 | 209 |
handle ERROR msg => |
210 |
cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name)); |
|
4866 | 211 |
|
212 |
||
29056 | 213 |
(* add_typedef: tactic interface *) |
4866 | 214 |
|
28662 | 215 |
fun add_typedef def opt_name typ set opt_morphs tac thy = |
6383 | 216 |
let |
17922 | 217 |
val name = the_default (#1 typ) opt_name; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
218 |
val (set, goal, _, typedef_result) = |
28662 | 219 |
prepare_typedef Syntax.check_term def name typ set opt_morphs thy; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
220 |
val inhabited = Goal.prove_global thy [] [] goal (K tac) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
221 |
handle ERROR msg => cat_error msg |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
222 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
223 |
in typedef_result inhabited thy end; |
4866 | 224 |
|
17339 | 225 |
|
29056 | 226 |
(* typedef: proof interface *) |
6383 | 227 |
|
17339 | 228 |
local |
229 |
||
230 |
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = |
|
11822 | 231 |
let |
29062 | 232 |
val (_, goal, goal_pat, typedef_result) = |
13443 | 233 |
prepare_typedef prep_term def name typ set opt_morphs thy; |
21352 | 234 |
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); |
29062 | 235 |
in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end; |
17339 | 236 |
|
237 |
in |
|
6383 | 238 |
|
28662 | 239 |
val typedef = gen_typedef Syntax.check_term; |
240 |
val typedef_cmd = gen_typedef Syntax.read_term; |
|
17339 | 241 |
|
19705 | 242 |
end; |
15259 | 243 |
|
244 |
||
245 |
||
6383 | 246 |
(** outer syntax **) |
247 |
||
29056 | 248 |
local structure P = OuterParse in |
6383 | 249 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26939
diff
changeset
|
250 |
val _ = OuterKeyword.keyword "morphisms"; |
24867 | 251 |
|
252 |
val _ = |
|
29056 | 253 |
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" |
254 |
OuterKeyword.thy_goal |
|
35202
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
255 |
(Scan.optional (P.$$$ "(" |-- |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
256 |
((P.$$$ "open" >> K false) -- Scan.option P.binding || |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
257 |
P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- |
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35238
diff
changeset
|
258 |
(P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- |
35202
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
259 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
260 |
>> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
261 |
Toplevel.print o Toplevel.theory_to_proof |
48721d3d77e7
typedef: slightly more precise treatment of binding;
wenzelm
parents:
35134
diff
changeset
|
262 |
(typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)))); |
6357 | 263 |
|
29056 | 264 |
end; |
265 |
||
33314 | 266 |
val setup = Typedef_Interpretation.init; |
25535 | 267 |
|
4866 | 268 |
end; |