src/HOL/Import/HOLLightCompat.thy
changeset 21404 eb85850d3eb7
parent 19064 bf19cc5a7899
child 35416 d8d7d1b785af