44 (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory |
44 (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory |
45 val alias: binding * string -> local_theory -> local_theory |
45 val alias: binding * string -> local_theory -> local_theory |
46 val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory |
46 val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory |
47 val type_alias: binding * string -> local_theory -> local_theory |
47 val type_alias: binding * string -> local_theory -> local_theory |
48 val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory |
48 val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory |
49 val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory |
|
50 val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> |
|
51 local_theory -> local_theory |
|
52 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
|
53 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
|
54 val theorems: string -> |
49 val theorems: string -> |
55 (Attrib.binding * Attrib.thms) list -> |
50 (Attrib.binding * Attrib.thms) list -> |
56 (binding * typ option * mixfix) list -> |
51 (binding * typ option * mixfix) list -> |
57 bool -> local_theory -> (string * thm list) list * local_theory |
52 bool -> local_theory -> (string * thm list) list * local_theory |
58 val theorems_cmd: string -> |
53 val theorems_cmd: string -> |
332 gen_alias Local_Theory.type_alias (K (K (fn c => (c, [])))); |
327 gen_alias Local_Theory.type_alias (K (K (fn c => (c, [])))); |
333 val type_alias_cmd = |
328 val type_alias_cmd = |
334 gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name); |
329 gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name); |
335 |
330 |
336 |
331 |
337 (* notation *) |
|
338 |
|
339 local |
|
340 |
|
341 fun gen_type_notation prep_type add mode args lthy = |
|
342 lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args); |
|
343 |
|
344 fun gen_notation prep_const add mode args lthy = |
|
345 lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args); |
|
346 |
|
347 in |
|
348 |
|
349 val type_notation = gen_type_notation (K I); |
|
350 val type_notation_cmd = |
|
351 gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false}); |
|
352 |
|
353 val notation = gen_notation (K I); |
|
354 val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false}); |
|
355 |
|
356 end; |
|
357 |
|
358 |
|
359 (* fact statements *) |
332 (* fact statements *) |
360 |
333 |
361 local |
334 local |
362 |
335 |
363 fun gen_theorems prep_fact prep_att add_fixes |
336 fun gen_theorems prep_fact prep_att add_fixes |