src/HOL/Extraction.thy
changeset 15542 ee6cd48cf840
parent 15531 08c8dad8e399
child 16121 a80aa66d2271