src/HOL/Library/Conditional_Parametricity.thy
changeset 83194 c2566f1548f4
parent 69605 a96320074298