src/HOL/MicroJava/DFA/Typing_Framework_err.thy
changeset 73929 7d15ebca4bb3
parent 69597 ff784d5a5bfb
equal deleted inserted replaced
73928:3b76524f5a85 73929:7d15ebca4bb3