equal
deleted
inserted
replaced
18 val abbrev: (string * bool -> binding * mixfix -> term * term -> |
18 val abbrev: (string * bool -> binding * mixfix -> term * term -> |
19 term list -> local_theory -> local_theory) -> |
19 term list -> local_theory -> local_theory) -> |
20 string * bool -> (binding * mixfix) * term -> local_theory -> |
20 string * bool -> (binding * mixfix) * term -> local_theory -> |
21 (term * term) * local_theory |
21 (term * term) * local_theory |
22 |
22 |
23 val theory_declaration: declaration -> local_theory -> local_theory |
23 val theory_declaration: bool -> declaration -> local_theory -> local_theory |
24 val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
24 val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> |
25 term list * term list -> local_theory -> (term * thm) * local_theory |
25 term list * term list -> local_theory -> (term * thm) * local_theory |
26 val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list -> |
26 val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list -> |
27 local_theory -> local_theory |
27 local_theory -> local_theory |
28 val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory |
28 val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory |
183 end; |
183 end; |
184 |
184 |
185 |
185 |
186 (** primitive theory operations **) |
186 (** primitive theory operations **) |
187 |
187 |
188 fun theory_declaration decl lthy = |
188 fun theory_declaration syntax decl lthy = |
189 let |
189 let |
190 val global_decl = Morphism.form |
190 val global_decl = Morphism.form |
191 (Morphism.transform (Local_Theory.global_morphism lthy) decl); |
191 (Morphism.transform (Local_Theory.global_morphism lthy) decl); |
192 in |
192 in |
193 lthy |
193 lthy |
194 |> Local_Theory.background_theory (Context.theory_map global_decl) |
194 |> Local_Theory.background_theory (Context.theory_map global_decl) |
195 |> Local_Theory.target (Context.proof_map global_decl) |
195 |> Local_Theory.target (Context.proof_map global_decl) |
|
196 |> not syntax ? Context.proof_map (Morphism.form decl) |
196 end; |
197 end; |
197 |
198 |
198 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
199 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
199 let |
200 let |
200 val (const, lthy2) = lthy |
201 val (const, lthy2) = lthy |