src/HOL/Extraction/Higman.thy
changeset 32115 8f10fb3bb46e
parent 31180 dae7be64d614
child 32960 69916a850301
equal deleted inserted replaced
32114:35084ad81bd4 32115:8f10fb3bb46e