40 local_theory -> (term * (bstring * thm)) * local_theory |
40 local_theory -> (term * (bstring * thm)) * local_theory |
41 val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term -> |
41 val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term -> |
42 local_theory -> local_theory |
42 local_theory -> local_theory |
43 val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> |
43 val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> |
44 local_theory -> local_theory |
44 local_theory -> local_theory |
45 val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
45 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
46 val notation_cmd: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
46 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
47 val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list |
47 val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list |
48 -> local_theory -> (bstring * thm list) list * local_theory |
48 -> local_theory -> (bstring * thm list) list * local_theory |
49 val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
49 val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
50 -> local_theory -> (bstring * thm list) list * local_theory |
50 -> local_theory -> (bstring * thm list) list * local_theory |
51 val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
51 val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
219 val abbreviation_cmd = gen_abbrev read_free_specification; |
219 val abbreviation_cmd = gen_abbrev read_free_specification; |
220 |
220 |
221 |
221 |
222 (* notation *) |
222 (* notation *) |
223 |
223 |
224 fun gen_notation prep_const mode args lthy = |
224 fun gen_notation prep_const add mode args lthy = |
225 lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args); |
225 lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args); |
226 |
226 |
227 val notation = gen_notation (K I); |
227 val notation = gen_notation (K I); |
228 val notation_cmd = gen_notation ProofContext.read_const; |
228 val notation_cmd = gen_notation ProofContext.read_const; |
229 |
229 |
230 |
230 |