70 val print_global_registrations: bool -> string -> theory -> unit |
70 val print_global_registrations: bool -> string -> theory -> unit |
71 val print_local_registrations': bool -> string -> Proof.context -> unit |
71 val print_local_registrations': bool -> string -> Proof.context -> unit |
72 val print_local_registrations: bool -> string -> Proof.context -> unit |
72 val print_local_registrations: bool -> string -> Proof.context -> unit |
73 |
73 |
74 val add_locale: bool -> bstring -> expr -> Element.context list -> theory |
74 val add_locale: bool -> bstring -> expr -> Element.context list -> theory |
75 -> Proof.context (*body context!*) * theory |
75 -> string * Proof.context (*body context!*) * theory |
76 val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory |
76 val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory |
77 -> Proof.context (*body context!*) * theory |
77 -> string * Proof.context (*body context!*) * theory |
78 |
78 |
79 (* Storing results *) |
79 (* Storing results *) |
80 val note_thmss: string -> xstring -> |
80 val note_thmss: string -> xstring -> |
81 ((string * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
81 ((string * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
82 theory -> ((string * thm list) list * (string * thm list) list) * (Proof.context * theory) |
82 theory -> ((string * thm list) list * (string * thm list) list) * (Proof.context * theory) |
1706 elems = map (fn e => (e, stamp ())) elems', |
1706 elems = map (fn e => (e, stamp ())) elems', |
1707 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), |
1707 params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), |
1708 lparams = map #1 (params_of body_elemss), |
1708 lparams = map #1 (params_of body_elemss), |
1709 abbrevs = [], |
1709 abbrevs = [], |
1710 regs = []}; |
1710 regs = []}; |
1711 in (ProofContext.transfer thy' body_ctxt, thy') end; |
1711 in (name, ProofContext.transfer thy' body_ctxt, thy') end; |
1712 |
1712 |
1713 in |
1713 in |
1714 |
1714 |
1715 val add_locale = gen_add_locale read_context intern_expr; |
1715 val add_locale = gen_add_locale read_context intern_expr; |
1716 val add_locale_i = gen_add_locale cert_context (K I); |
1716 val add_locale_i = gen_add_locale cert_context (K I); |
1717 |
1717 |
1718 end; |
1718 end; |
1719 |
1719 |
1720 val _ = Context.add_setup |
1720 val _ = Context.add_setup |
1721 (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> snd #> |
1721 (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #> #3 #> |
1722 add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> snd); |
1722 add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]] #> #3); |
1723 |
1723 |
1724 |
1724 |
1725 |
1725 |
1726 (** locale goals **) |
1726 (** locale goals **) |
1727 |
1727 |