src/HOL/IMP/OO.thy
changeset 68048 0b4fb9fd91b1
parent 67406 23307fd33906
child 74101 d804e93ae9ff
equal deleted inserted replaced
68045:ce8ad77cd3fa 68048:0b4fb9fd91b1