src/HOL/Import/HOLLightCompat.thy
changeset 29270 0eade173f77e
parent 19064 bf19cc5a7899
child 35416 d8d7d1b785af