src/HOL/Extraction.thy
changeset 64427 195242d16c03
parent 62922 96691631c1eb
child 69593 3dda49e08b9d
equal deleted inserted replaced
64425:b17acc1834e3 64427:195242d16c03