src/HOL/Extraction.thy
changeset 29380 a9ee3475abf4
parent 28797 9dcd32ee5dbe
child 29930 80a9a55b0a0e