src/HOL/Extraction.thy
changeset 78517 28c1f4f5335f
parent 70847 e62d5433bb47