equal
deleted
inserted
replaced
257 let |
257 let |
258 fun build_alpha alpha = |
258 fun build_alpha alpha = |
259 let |
259 let |
260 val ty = domain_type (fastype_of alpha); |
260 val ty = domain_type (fastype_of alpha); |
261 val var = Free("x", ty); |
261 val var = Free("x", ty); |
|
262 val var2 = Free("y", ty); |
262 in |
263 in |
263 alpha $ var $ var |
264 ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var))) |
264 end |
265 end; |
265 val eqs = map build_alpha alphas |
266 val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas) |
266 in |
267 in |
267 @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs |
268 Logic.mk_conjunction |
268 end |
269 (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs, |
269 *} |
270 @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs) |
270 |
271 end |
271 |
272 *} |
272 end |
273 |
|
274 |
|
275 end |