src/HOL/Extraction.thy
changeset 13477 6f9111705d4f
parent 13468 71118807d303
child 13599 cfdf7e4cd0d2