src/HOL/Metis.thy
changeset 73821 9ead8d9be3ab
parent 69605 a96320074298
child 77263 27be31d7ad88
equal deleted inserted replaced
73820:745e2cd1f5f5 73821:9ead8d9be3ab