src/HOL/IMP/OO.thy
changeset 44821 a92f65e174cf
parent 43158 686fa0a0696e
child 47818 151d137f1095
equal deleted inserted replaced
44797:e0da66339e47 44821:a92f65e174cf