src/HOL/Library/conditional_parametricity.ML
changeset 76684 3eda063a20a4
parent 76051 854e9223767f
child 78465 4dffc47b7e91