equal
deleted
inserted
replaced
89 end; |
89 end; |
90 |
90 |
91 *} |
91 *} |
92 |
92 |
93 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
93 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
94 |
|
95 ML {* |
94 ML {* |
96 (* Currently needs just one full_tname to access Datatype *) |
95 (* Currently needs just one full_tname to access Datatype *) |
97 fun define_fv_alpha full_tname bindsall lthy = |
96 fun define_fv_alpha full_tname bindsall lthy = |
98 let |
97 let |
99 val thy = ProofContext.theory_of lthy; |
98 val thy = ProofContext.theory_of lthy; |
251 in |
250 in |
252 Variable.export ctxt' ctxt thms |
251 Variable.export ctxt' ctxt thms |
253 end |
252 end |
254 *} |
253 *} |
255 |
254 |
256 end |
255 ML {* |
|
256 fun build_alpha_refl_gl alphas = |
|
257 let |
|
258 fun build_alpha alpha = |
|
259 let |
|
260 val ty = domain_type (fastype_of alpha); |
|
261 val var = Free("x", ty); |
|
262 in |
|
263 alpha $ var $ var |
|
264 end |
|
265 val eqs = map build_alpha alphas |
|
266 in |
|
267 @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs |
|
268 end |
|
269 *} |
|
270 |
|
271 |
|
272 end |