src/HOL/IMP/OO.thy
changeset 44246 380a4677c55d
parent 43158 686fa0a0696e
child 47818 151d137f1095
equal deleted inserted replaced
44245:45fb4b29c267 44246:380a4677c55d