src/HOL/MicroJava/DFA/Err.thy
changeset 34040 37af49de030a
parent 33954 1bc3b688548c
child 35102 cc7a0b9f938c