src/HOL/MicroJava/DFA/Err.thy
changeset 42148 d596e7bb251f
parent 41541 1fa4725c4656
child 42150 b0c0638c4aad