src/HOL/Import/HOLLightCompat.thy
changeset 23024 70435ffe077d
parent 19064 bf19cc5a7899
child 35416 d8d7d1b785af