equal
deleted
inserted
replaced
455 let |
455 let |
456 val parametricity_thm_map_filter = |
456 val parametricity_thm_map_filter = |
457 Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify |
457 Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify |
458 (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt; |
458 (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt; |
459 in |
459 in |
460 map_filter (parametricity_thm_map_filter o Thm.transfer (Proof_Context.theory_of ctxt)) |
460 map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt) |
461 (Transfer.get_transfer_raw ctxt) |
461 (Transfer.get_transfer_raw ctxt) |
462 end; |
462 end; |
463 |
463 |
464 (* Provers *) |
464 (* Provers *) |
465 (* Tries to prove a parametricity theorem without conditions, returns the last goal_state as thm *) |
465 (* Tries to prove a parametricity theorem without conditions, returns the last goal_state as thm *) |