src/HOL/MicroJava/DFA/LBVCorrect.thy
changeset 43811 402e1a0d93d9
parent 33954 1bc3b688548c
child 58886 8a6cac7c7247