src/HOL/Extraction.thy
changeset 29152 89b0803404d7
parent 28797 9dcd32ee5dbe
child 29930 80a9a55b0a0e
equal deleted inserted replaced
29151:fa5224eb28a5 29152:89b0803404d7