src/HOL/Library/Conditional_Parametricity.thy
changeset 79570 7254253f2ec7
parent 69605 a96320074298