src/HOL/Extraction.thy
changeset 15789 4cb16144c81b
parent 15531 08c8dad8e399
child 16121 a80aa66d2271