src/HOL/MicroJava/DFA/Err.thy
changeset 39244 d31c03a34f76
parent 35416 d8d7d1b785af
child 39758 b8a53e3a0ee2
equal deleted inserted replaced
39243:307e3d07d19f 39244:d31c03a34f76