src/HOL/Extraction.thy
changeset 22175 d9e3e4c30d6b
parent 20941 beedcae49096
child 22281 23e0fde84cb7