author | wenzelm |
Thu, 18 Apr 2013 17:07:01 +0200 | |
changeset 51717 | 9e7d1c139569 |
parent 51484 | 49eb8d73ae10 |
child 52087 | f3075fc4f5f6 |
permissions | -rw-r--r-- |
40107 | 1 |
(* Title: HOL/Tools/Function/partial_function.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
4 |
Partial function definitions based on least fixed points in ccpos. |
|
5 |
*) |
|
6 |
||
7 |
signature PARTIAL_FUNCTION = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
43080 | 10 |
val init: string -> term -> term -> thm -> thm option -> declaration |
40107 | 11 |
|
12 |
val add_partial_function: string -> (binding * typ option * mixfix) list -> |
|
13 |
Attrib.binding * term -> local_theory -> local_theory |
|
14 |
||
15 |
val add_partial_function_cmd: string -> (binding * string option * mixfix) list -> |
|
16 |
Attrib.binding * string -> local_theory -> local_theory |
|
17 |
end; |
|
18 |
||
19 |
||
20 |
structure Partial_Function: PARTIAL_FUNCTION = |
|
21 |
struct |
|
22 |
||
23 |
(*** Context Data ***) |
|
24 |
||
43080 | 25 |
datatype setup_data = Setup_Data of |
26 |
{fixp: term, |
|
27 |
mono: term, |
|
28 |
fixp_eq: thm, |
|
29 |
fixp_induct: thm option}; |
|
30 |
||
40107 | 31 |
structure Modes = Generic_Data |
32 |
( |
|
43080 | 33 |
type T = setup_data Symtab.table; |
40107 | 34 |
val empty = Symtab.empty; |
35 |
val extend = I; |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41117
diff
changeset
|
36 |
fun merge data = Symtab.merge (K true) data; |
40107 | 37 |
) |
38 |
||
43080 | 39 |
fun init mode fixp mono fixp_eq fixp_induct phi = |
40107 | 40 |
let |
41 |
val term = Morphism.term phi; |
|
43080 | 42 |
val thm = Morphism.thm phi; |
43 |
val data' = Setup_Data |
|
44 |
{fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq, |
|
45 |
fixp_induct=Option.map thm fixp_induct}; |
|
40107 | 46 |
in |
42949
618adb3584e5
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
krauss
parents:
42495
diff
changeset
|
47 |
Modes.map (Symtab.update (mode, data')) |
40107 | 48 |
end |
49 |
||
50 |
val known_modes = Symtab.keys o Modes.get o Context.Proof; |
|
51 |
val lookup_mode = Symtab.lookup o Modes.get o Context.Proof; |
|
52 |
||
53 |
||
54 |
structure Mono_Rules = Named_Thms |
|
55 |
( |
|
45294 | 56 |
val name = @{binding partial_function_mono}; |
40107 | 57 |
val description = "monotonicity rules for partial function definitions"; |
58 |
); |
|
59 |
||
60 |
||
61 |
(*** Automated monotonicity proofs ***) |
|
62 |
||
63 |
fun strip_cases ctac = ctac #> Seq.map snd; |
|
64 |
||
65 |
(*rewrite conclusion with k-th assumtion*) |
|
66 |
fun rewrite_with_asm_tac ctxt k = |
|
45403 | 67 |
Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
40107 | 68 |
Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt; |
69 |
||
70 |
fun dest_case thy t = |
|
71 |
case strip_comb t of |
|
72 |
(Const (case_comb, _), args) => |
|
73 |
(case Datatype.info_of_case thy case_comb of |
|
74 |
NONE => NONE |
|
75 |
| SOME {case_rewrites, ...} => |
|
76 |
let |
|
77 |
val lhs = prop_of (hd case_rewrites) |
|
78 |
|> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst; |
|
79 |
val arity = length (snd (strip_comb lhs)); |
|
80 |
val conv = funpow (length args - arity) Conv.fun_conv |
|
81 |
(Conv.rewrs_conv (map mk_meta_eq case_rewrites)); |
|
82 |
in |
|
83 |
SOME (nth args (arity - 1), conv) |
|
84 |
end) |
|
85 |
| _ => NONE; |
|
86 |
||
87 |
(*split on case expressions*) |
|
88 |
val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} => |
|
89 |
SUBGOAL (fn (t, i) => case t of |
|
90 |
_ $ (_ $ Abs (_, _, body)) => |
|
42361 | 91 |
(case dest_case (Proof_Context.theory_of ctxt) body of |
40107 | 92 |
NONE => no_tac |
93 |
| SOME (arg, conv) => |
|
94 |
let open Conv in |
|
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41472
diff
changeset
|
95 |
if Term.is_open arg then no_tac |
40107 | 96 |
else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE []) |
97 |
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0) |
|
98 |
THEN_ALL_NEW etac @{thm thin_rl} |
|
99 |
THEN_ALL_NEW (CONVERSION |
|
100 |
(params_conv ~1 (fn ctxt' => |
|
101 |
arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i |
|
102 |
end) |
|
103 |
| _ => no_tac) 1); |
|
104 |
||
105 |
(*monotonicity proof: apply rules + split case expressions*) |
|
106 |
fun mono_tac ctxt = |
|
107 |
K (Local_Defs.unfold_tac ctxt [@{thm curry_def}]) |
|
108 |
THEN' (TRY o REPEAT_ALL_NEW |
|
109 |
(resolve_tac (Mono_Rules.get ctxt) |
|
110 |
ORELSE' split_cases_tac ctxt)); |
|
111 |
||
112 |
||
113 |
(*** Auxiliary functions ***) |
|
114 |
||
115 |
(*positional instantiation with computed type substitution. |
|
116 |
internal version of attribute "[of s t u]".*) |
|
117 |
fun cterm_instantiate' cts thm = |
|
118 |
let |
|
119 |
val thy = Thm.theory_of_thm thm; |
|
120 |
val vs = rev (Term.add_vars (prop_of thm) []) |
|
121 |
|> map (Thm.cterm_of thy o Var); |
|
122 |
in |
|
123 |
cterm_instantiate (zip_options vs cts) thm |
|
124 |
end; |
|
125 |
||
126 |
(*Returns t $ u, but instantiates the type of t to make the |
|
127 |
application type correct*) |
|
128 |
fun apply_inst ctxt t u = |
|
129 |
let |
|
42361 | 130 |
val thy = Proof_Context.theory_of ctxt; |
40107 | 131 |
val T = domain_type (fastype_of t); |
132 |
val T' = fastype_of u; |
|
42388 | 133 |
val subst = Sign.typ_match thy (T, T') Vartab.empty |
40107 | 134 |
handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u]) |
135 |
in |
|
136 |
map_types (Envir.norm_type subst) t $ u |
|
137 |
end; |
|
138 |
||
139 |
fun head_conv cv ct = |
|
140 |
if can Thm.dest_comb ct then Conv.fun_conv (head_conv cv) ct else cv ct; |
|
141 |
||
142 |
||
143 |
(*** currying transformation ***) |
|
144 |
||
145 |
fun curry_const (A, B, C) = |
|
146 |
Const (@{const_name Product_Type.curry}, |
|
147 |
[HOLogic.mk_prodT (A, B) --> C, A, B] ---> C); |
|
148 |
||
149 |
fun mk_curry f = |
|
150 |
case fastype_of f of |
|
151 |
Type ("fun", [Type (_, [S, T]), U]) => |
|
152 |
curry_const (S, T, U) $ f |
|
153 |
| T => raise TYPE ("mk_curry", [T], [f]); |
|
154 |
||
155 |
(* iterated versions. Nonstandard left-nested tuples arise naturally |
|
156 |
from "split o split o split"*) |
|
157 |
fun curry_n arity = funpow (arity - 1) mk_curry; |
|
158 |
fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split; |
|
159 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
160 |
val curry_uncurry_ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
161 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
162 |
addsimps [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}]) |
40107 | 163 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
164 |
val split_conv_ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
165 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
166 |
addsimps [@{thm Product_Type.split_conv}]); |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
167 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
168 |
fun mk_curried_induct args ctxt ccurry cuncurry rule = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
169 |
let |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
170 |
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
171 |
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
172 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
173 |
val split_paired_all_conv = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
174 |
Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all})) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
175 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
176 |
val split_params_conv = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
177 |
Conv.params_conv ~1 (fn ctxt' => |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
178 |
Conv.implies_conv split_paired_all_conv Conv.all_conv) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
179 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
180 |
val inst_rule = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
181 |
cterm_instantiate' [SOME cuncurry, NONE, SOME ccurry] rule |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
182 |
|
51484
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
183 |
val P_rangeT = |
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
184 |
Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
185 |
|> Term.head_of |> Term.dest_Var |> snd |> range_type |
49eb8d73ae10
allow induction predicates with arbitrary arity (not just binary)
krauss
parents:
46961
diff
changeset
|
186 |
val PT = map (snd o dest_Free) args ---> P_rangeT |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
187 |
val x_inst = cert (foldl1 HOLogic.mk_prod args) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
188 |
val P_inst = cert (uncurry_n (length args) (Free (P, PT))) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
189 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
190 |
val inst_rule' = inst_rule |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
191 |
|> Tactic.rule_by_tactic ctxt |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
192 |
(Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4 |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
193 |
THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
194 |
THEN CONVERSION (split_params_conv ctxt |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
195 |
then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
196 |
|> Drule.instantiate' [] [NONE, NONE, SOME P_inst, SOME x_inst] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
197 |
|> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
198 |
|> singleton (Variable.export ctxt' ctxt) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
199 |
in |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
200 |
inst_rule' |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
201 |
end; |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
202 |
|
40107 | 203 |
|
204 |
(*** partial_function definition ***) |
|
205 |
||
206 |
fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy = |
|
207 |
let |
|
43080 | 208 |
val setup_data = the (lookup_mode lthy mode) |
40107 | 209 |
handle Option.Option => error (cat_lines ["Unknown mode " ^ quote mode ^ ".", |
210 |
"Known modes are " ^ commas_quote (known_modes lthy) ^ "."]); |
|
43080 | 211 |
val Setup_Data {fixp, mono, fixp_eq, fixp_induct} = setup_data; |
40107 | 212 |
|
213 |
val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy; |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
214 |
val ((_, plain_eqn), args_ctxt) = Variable.focus eqn lthy; |
40107 | 215 |
|
216 |
val ((f_binding, fT), mixfix) = the_single fixes; |
|
217 |
val fname = Binding.name_of f_binding; |
|
218 |
||
42361 | 219 |
val cert = cterm_of (Proof_Context.theory_of lthy); |
40107 | 220 |
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); |
221 |
val (head, args) = strip_comb lhs; |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
222 |
val argnames = map (fst o dest_Free) args; |
40107 | 223 |
val F = fold_rev lambda (head :: args) rhs; |
224 |
||
225 |
val arity = length args; |
|
226 |
val (aTs, bTs) = chop arity (binder_types fT); |
|
227 |
||
228 |
val tupleT = foldl1 HOLogic.mk_prodT aTs; |
|
229 |
val fT_uc = tupleT :: bTs ---> body_type fT; |
|
230 |
val f_uc = Var ((fname, 0), fT_uc); |
|
231 |
val x_uc = Var (("x", 0), tupleT); |
|
232 |
val uncurry = lambda head (uncurry_n arity head); |
|
233 |
val curry = lambda f_uc (curry_n arity f_uc); |
|
234 |
||
235 |
val F_uc = |
|
236 |
lambda f_uc (uncurry_n arity (F $ curry_n arity f_uc)); |
|
237 |
||
238 |
val mono_goal = apply_inst lthy mono (lambda f_uc (F_uc $ f_uc $ x_uc)) |
|
239 |
|> HOLogic.mk_Trueprop |
|
240 |
|> Logic.all x_uc; |
|
241 |
||
242 |
val mono_thm = Goal.prove_internal [] (cert mono_goal) |
|
243 |
(K (mono_tac lthy 1)) |
|
244 |
|> Thm.forall_elim (cert x_uc); |
|
245 |
||
246 |
val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc); |
|
247 |
val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname)); |
|
248 |
val ((f, (_, f_def)), lthy') = Local_Theory.define |
|
249 |
((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy; |
|
250 |
||
251 |
val eqn = HOLogic.mk_eq (list_comb (f, args), |
|
252 |
Term.betapplys (F, f :: args)) |
|
253 |
|> HOLogic.mk_Trueprop; |
|
254 |
||
255 |
val unfold = |
|
256 |
(cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq |
|
257 |
OF [mono_thm, f_def]) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51484
diff
changeset
|
258 |
|> Tactic.rule_by_tactic lthy (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy) 1); |
40107 | 259 |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
260 |
val mk_raw_induct = |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
261 |
mk_curried_induct args args_ctxt (cert curry) (cert uncurry) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
262 |
#> singleton (Variable.export args_ctxt lthy) |
45008
8b74cfea913a
match types when applying mono_thm -- previous export generalizes type variables;
krauss
parents:
43083
diff
changeset
|
263 |
#> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [mono_thm, f_def]) |
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
264 |
#> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames)) |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
265 |
|
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
266 |
val raw_induct = Option.map mk_raw_induct fixp_induct |
40107 | 267 |
val rec_rule = let open Conv in |
268 |
Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ => |
|
269 |
CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1 |
|
270 |
THEN rtac @{thm refl} 1) end; |
|
271 |
in |
|
272 |
lthy' |
|
273 |
|> Local_Theory.note (eq_abinding, [rec_rule]) |
|
274 |
|-> (fn (_, rec') => |
|
40180 | 275 |
Spec_Rules.add Spec_Rules.Equational ([f], rec') |
276 |
#> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd) |
|
43083
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
277 |
|> (case raw_induct of NONE => I | SOME thm => |
df41a5762c3d
generate raw induction rule as instance of generic rule with careful treatment of currying
krauss
parents:
43080
diff
changeset
|
278 |
Local_Theory.note ((Binding.qualify true fname (Binding.name "raw_induct"), []), [thm]) #> snd) |
40107 | 279 |
end; |
280 |
||
281 |
val add_partial_function = gen_add_partial_function Specification.check_spec; |
|
282 |
val add_partial_function_cmd = gen_add_partial_function Specification.read_spec; |
|
283 |
||
46949 | 284 |
val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"}; |
40107 | 285 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
286 |
val _ = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
287 |
Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
288 |
((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec))) |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
289 |
>> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec)); |
40107 | 290 |
|
291 |
||
292 |
val setup = Mono_Rules.setup; |
|
293 |
||
294 |
end |