src/HOL/Extraction.thy
changeset 29465 b2cfb5d0a59e
parent 28797 9dcd32ee5dbe
child 29930 80a9a55b0a0e
equal deleted inserted replaced
29464:c0d225a7f6ff 29465:b2cfb5d0a59e