src/HOL/Extraction.thy
changeset 21404 eb85850d3eb7
parent 20941 beedcae49096
child 22281 23e0fde84cb7
equal deleted inserted replaced
21403:dd58f13a8eb4 21404:eb85850d3eb7