src/HOL/Extraction/Util.thy
changeset 32115 8f10fb3bb46e
parent 25421 1c5b8d54a339
child 32960 69916a850301
equal deleted inserted replaced
32114:35084ad81bd4 32115:8f10fb3bb46e