src/HOL/Library/conditional_parametricity.ML
changeset 74877 1a5d4586b6b0
parent 74545 6c123914883a
child 76051 854e9223767f