src/HOL/MicroJava/DFA/Err.thy
changeset 62117 86a31308a8e1
parent 61952 546958347e05
child 63170 eae6549dbea2