src/HOL/Extraction.thy
changeset 72283 c0d04c740b8a
parent 70847 e62d5433bb47