equal
deleted
inserted
replaced
18 |
18 |
19 (* wrapper for define *) |
19 (* wrapper for define *) |
20 fun define name mx attr rhs lthy = |
20 fun define name mx attr rhs lthy = |
21 let |
21 let |
22 val ((rhs, (_ , thm)), lthy') = |
22 val ((rhs, (_ , thm)), lthy') = |
23 LocalTheory.define Thm.internalK ((name, mx), (attr, rhs)) lthy |
23 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
24 in |
24 in |
25 ((rhs, thm), lthy') |
25 ((rhs, thm), lthy') |
26 end |
26 end |
27 |
27 |
28 |
28 |
138 |
138 |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
139 val ((trm, thm), lthy') = define nconst_bname mx attr absrep_trm lthy |
140 |
140 |
141 val nconst_str = Binding.name_of nconst_bname |
141 val nconst_str = Binding.name_of nconst_bname |
142 val qcinfo = {qconst = trm, rconst = rhs} |
142 val qcinfo = {qconst = trm, rconst = rhs} |
143 val lthy'' = LocalTheory.declaration true |
143 val lthy'' = Local_Theory.declaration true |
144 (fn phi => qconsts_update_generic nconst_str |
144 (fn phi => qconsts_update_generic nconst_str |
145 (qconsts_transfer phi qcinfo)) lthy' |
145 (qconsts_transfer phi qcinfo)) lthy' |
146 in |
146 in |
147 ((trm, thm), lthy'') |
147 ((trm, thm), lthy'') |
148 end |
148 end |
157 (* - a meta-equation defining the constant, *) |
157 (* - a meta-equation defining the constant, *) |
158 (* and the attributes of for this meta-equality *) |
158 (* and the attributes of for this meta-equality *) |
159 |
159 |
160 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
160 fun quotdef ((bind, qty, mx), (attr, prop)) lthy = |
161 let |
161 let |
162 val (_, prop') = Primitive_Defs.dest_def lthy (K true) (K false) (K false) prop |
162 val (_, prop') = LocalDefs.cert_def lthy prop |
163 val (_, rhs) = Primitive_Defs.abs_def prop' |
163 val (_, rhs) = Primitive_Defs.abs_def prop' |
164 in |
164 in |
165 make_def bind qty mx attr rhs lthy |
165 make_def bind qty mx attr rhs lthy |
166 end |
166 end |
167 |
167 |