src/HOL/Extraction.thy
changeset 33890 a87ad4be59a4
parent 33723 14d0dadd9517
child 34913 d8cb720c9c53