author | haftmann |
Sat, 14 Nov 2015 08:45:52 +0100 | |
changeset 61672 | 87203a0f0041 |
parent 61670 | 301e0b4ecd45 |
child 61673 | fd4ac1530d63 |
permissions | -rw-r--r-- |
61669 | 1 |
(* Title: Pure/Isar/interpretation.ML |
2 |
Author: Clemens Ballarin, TU Muenchen |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
61669 | 4 |
|
5 |
Locale interpretation. |
|
6 |
*) |
|
7 |
||
8 |
signature INTERPRETATION = |
|
9 |
sig |
|
10 |
val interpret: Expression.expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state |
|
11 |
val interpret_cmd: Expression.expression -> (Attrib.binding * string) list -> |
|
12 |
bool -> Proof.state -> Proof.state |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
13 |
val ephemeral_interpretation: Expression.expression_i -> (Attrib.binding * term) list -> |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
14 |
local_theory -> Proof.state |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
15 |
val permanent_interpretation: Expression.expression_i -> |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
16 |
(Attrib.binding * ((binding * mixfix) * term)) list -> (Attrib.binding * term) list -> |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
17 |
local_theory -> Proof.state |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
18 |
val permanent_interpretation_cmd: Expression.expression -> |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
19 |
(Attrib.binding * ((binding * mixfix) * string)) list -> (Attrib.binding * string) list -> |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
20 |
local_theory -> Proof.state |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
21 |
|
61669 | 22 |
val interpretation: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state |
23 |
val interpretation_cmd: Expression.expression -> (Attrib.binding * string) list -> |
|
24 |
local_theory -> Proof.state |
|
25 |
val sublocale: Expression.expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state |
|
26 |
val sublocale_cmd: Expression.expression -> (Attrib.binding * string) list -> local_theory -> Proof.state |
|
27 |
val sublocale_global: string -> Expression.expression_i -> |
|
28 |
(Attrib.binding * term) list -> theory -> Proof.state |
|
29 |
val sublocale_global_cmd: xstring * Position.T -> Expression.expression -> |
|
30 |
(Attrib.binding * string) list -> theory -> Proof.state |
|
31 |
end; |
|
32 |
||
33 |
structure Interpretation : INTERPRETATION = |
|
34 |
struct |
|
35 |
||
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
36 |
(** reading **) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
37 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
38 |
local |
61669 | 39 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
40 |
fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
41 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
42 |
(*reading*) |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
43 |
val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
44 |
val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
45 |
val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt deps_ctxt; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
46 |
val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
47 |
val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
48 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
49 |
(*defining*) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
50 |
val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
51 |
((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
52 |
val (defs, forked_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
53 |
val def_ctxt = Proof_Context.transfer (Proof_Context.theory_of forked_ctxt) expr_ctxt; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
54 |
val def_eqns = defs |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
55 |
|> map (Thm.symmetric o |
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
56 |
Morphism.thm (Local_Theory.standard_morphism forked_ctxt def_ctxt) o snd o snd); |
61669 | 57 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
58 |
(*setting up proof*) |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
59 |
val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
60 |
val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
61 |
val export' = Variable.export_morphism goal_ctxt def_ctxt; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
62 |
in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
61669 | 63 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
64 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
65 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
66 |
val cert_interpretation = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
67 |
prep_interpretation Expression.cert_goal_expression (K I) (K I) (K I); |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
68 |
|
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
69 |
val read_interpretation = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
70 |
prep_interpretation Expression.read_goal_expression Syntax.parse_term Syntax.parse_prop Attrib.check_src; |
61669 | 71 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
72 |
end; |
61669 | 73 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
74 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
75 |
(** common interpretation machinery **) |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
76 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
77 |
local |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
78 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
79 |
fun meta_rewrite eqns ctxt = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
80 |
(map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt); |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
81 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
82 |
fun note_eqns_register note activate deps witss def_eqns eqns attrss export export' ctxt = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
83 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
84 |
val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
85 |
:: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
86 |
val (eqns', ctxt') = ctxt |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
87 |
|> note Thm.theoremK facts |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
88 |
|-> meta_rewrite; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
89 |
val dep_morphs = map2 (fn (dep, morph) => fn wits => |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
90 |
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
91 |
fun activate' dep_morph ctxt = activate dep_morph |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
92 |
(Option.map (rpair true) (Element.eq_morphism (Proof_Context.theory_of ctxt) eqns')) export ctxt; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
93 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
94 |
ctxt' |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
95 |
|> fold activate' dep_morphs |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
96 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
97 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
98 |
in |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
99 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
100 |
fun generic_interpretation_with_defs prep_interpretation setup_proof note add_registration |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
101 |
expression raw_defs raw_eqns initial_ctxt = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
102 |
let |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
103 |
val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
104 |
prep_interpretation expression raw_defs raw_eqns initial_ctxt; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
105 |
fun after_qed witss eqns = |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
106 |
note_eqns_register note add_registration deps witss def_eqns eqns attrss export export'; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
107 |
in setup_proof after_qed propss eqns goal_ctxt end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
108 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
109 |
fun generic_interpretation prep_interpretation setup_proof note add_registration expression = |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
110 |
generic_interpretation_with_defs prep_interpretation setup_proof note add_registration expression []; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
111 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
112 |
end; |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
113 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
114 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
115 |
(** first dimension: proof vs. local theory **) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
116 |
|
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
117 |
local |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
118 |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
119 |
(* proof *) |
61669 | 120 |
|
121 |
fun gen_interpret prep_interpretation expression raw_eqns int state = |
|
122 |
let |
|
123 |
val _ = Proof.assert_forward_or_chain state; |
|
124 |
val ctxt = Proof.context_of state; |
|
125 |
fun lift_after_qed after_qed witss eqns = |
|
126 |
Proof.map_context (after_qed witss eqns) #> Proof.reset_facts; |
|
127 |
fun setup_proof after_qed propss eqns goal_ctxt = |
|
128 |
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" |
|
129 |
propss eqns goal_ctxt int state; |
|
130 |
in |
|
131 |
generic_interpretation prep_interpretation setup_proof |
|
132 |
Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression raw_eqns ctxt |
|
133 |
end; |
|
134 |
||
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
135 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
136 |
(* local theory *) |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
137 |
|
61669 | 138 |
fun gen_local_theory_interpretation prep_interpretation activate expression raw_eqns lthy = |
139 |
generic_interpretation prep_interpretation Element.witness_proof_eqs |
|
140 |
Local_Theory.notes_kind (activate lthy) expression raw_eqns lthy; |
|
141 |
||
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
142 |
fun gen_interpretation prep_interpretation expression raw_defs raw_eqns = |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
143 |
Local_Theory.assert_bottom true |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
144 |
#> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
145 |
Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns |
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
146 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
147 |
|
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
148 |
(** second dimension: relation to underlying target **) |
61669 | 149 |
|
150 |
fun subscribe_or_activate lthy = |
|
151 |
if Named_Target.is_theory lthy |
|
152 |
then Local_Theory.subscription |
|
153 |
else Locale.activate_fragment; |
|
154 |
||
155 |
fun subscribe_locale_only lthy = |
|
156 |
let |
|
157 |
val _ = |
|
158 |
if Named_Target.is_theory lthy |
|
159 |
then error "Not possible on level of global theory" |
|
160 |
else (); |
|
161 |
in Local_Theory.subscription end; |
|
162 |
||
163 |
||
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
164 |
(** special case: global sublocale command **) |
61669 | 165 |
|
166 |
fun gen_sublocale_global prep_loc prep_interpretation |
|
167 |
raw_locale expression raw_eqns thy = |
|
168 |
let |
|
169 |
val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
|
170 |
fun setup_proof after_qed = |
|
171 |
Element.witness_proof_eqs |
|
172 |
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
|
173 |
in |
|
174 |
lthy |> |
|
175 |
generic_interpretation prep_interpretation setup_proof |
|
176 |
Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns |
|
177 |
end; |
|
178 |
||
179 |
in |
|
180 |
||
181 |
||
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
182 |
(** interfaces **) |
61669 | 183 |
|
184 |
fun interpret x = gen_interpret cert_interpretation x; |
|
185 |
fun interpret_cmd x = gen_interpret read_interpretation x; |
|
186 |
||
187 |
fun ephemeral_interpretation x = |
|
188 |
gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x; |
|
189 |
||
61672
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
190 |
fun permanent_interpretation x = gen_interpretation cert_interpretation x; |
87203a0f0041
tuned -- share implementations as far as appropriate
haftmann
parents:
61670
diff
changeset
|
191 |
fun permanent_interpretation_cmd x = gen_interpretation read_interpretation x; |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61669
diff
changeset
|
192 |
|
61669 | 193 |
fun interpretation x = |
194 |
gen_local_theory_interpretation cert_interpretation subscribe_or_activate x; |
|
195 |
fun interpretation_cmd x = |
|
196 |
gen_local_theory_interpretation read_interpretation subscribe_or_activate x; |
|
197 |
||
198 |
fun sublocale x = |
|
199 |
gen_local_theory_interpretation cert_interpretation subscribe_locale_only x; |
|
200 |
fun sublocale_cmd x = |
|
201 |
gen_local_theory_interpretation read_interpretation subscribe_locale_only x; |
|
202 |
||
203 |
fun sublocale_global x = gen_sublocale_global (K I) cert_interpretation x; |
|
204 |
fun sublocale_global_cmd x = gen_sublocale_global Locale.check read_interpretation x; |
|
205 |
||
206 |
end; |
|
207 |
||
208 |
end; |