src/HOL/Library/conditional_parametricity.ML
changeset 76597 faea52979f54
parent 76051 854e9223767f
child 78465 4dffc47b7e91