src/HOL/Import/HOLLight/hollight.imp
changeset 36746 6e7704471eaa
parent 35267 8dfd816713c6
child 37387 3581483cca6c
equal deleted inserted replaced
36745:403585a89772 36746:6e7704471eaa