src/HOL/Extraction.thy
changeset 21087 3e56528a39f7
parent 20941 beedcae49096
child 22281 23e0fde84cb7
equal deleted inserted replaced
21086:fe9f43a1e5bd 21087:3e56528a39f7