src/ZF/IMP/Equiv.ML
changeset 2877 6476784dba1c
parent 2496 40efb87985b5
child 4091 771b1f6422a8