changeset 67399 | eab6ce8368fa |
parent 66251 | cd935b7cb3fb |
child 68782 | 8ff34c1ad580 |
--- a/src/HOL/Library/Mapping.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Library/Mapping.thy Wed Jan 10 15:25:09 2018 +0100 @@ -223,7 +223,7 @@ lemma [transfer_rule]: assumes [transfer_rule]: "bi_total A" and [transfer_rule]: "bi_unique B" - shows "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal" + shows "(pcr_mapping A B ===> pcr_mapping A B ===> (=)) HOL.eq HOL.equal" unfolding equal by transfer_prover lemma of_alist_transfer [transfer_rule]: