src/HOL/IMP/OO.thy
changeset 43665 573d1272f36d
parent 43158 686fa0a0696e
child 47818 151d137f1095
equal deleted inserted replaced
43664:47af50b0c8c5 43665:573d1272f36d