equal
deleted
inserted
replaced
344 fun build_eqvt_gl pi frees fnctn ctxt = |
344 fun build_eqvt_gl pi frees fnctn ctxt = |
345 let |
345 let |
346 val typ = domain_type (fastype_of fnctn); |
346 val typ = domain_type (fastype_of fnctn); |
347 val arg = the (AList.lookup (op=) frees typ); |
347 val arg = the (AList.lookup (op=) frees typ); |
348 in |
348 in |
349 ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
349 ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt) |
350 end |
350 end |
351 *} |
351 *} |
352 |
352 |
353 ML {* |
353 ML {* |
354 fun prove_eqvt tys ind simps funs ctxt = |
354 fun prove_eqvt tys ind simps funs ctxt = |