src/HOL/MicroJava/BV/Err.thy
changeset 12395 d6913de7655f
parent 11549 e7265e70fd7c
child 12516 d09d0f160888
equal deleted inserted replaced
12394:b20a37eb8338 12395:d6913de7655f