src/HOL/MicroJava/J/Decl.thy
changeset 45920 ddbe94f7242c
parent 42463 f270e3e18be5
child 58886 8a6cac7c7247
equal deleted inserted replaced
45919:2cae3d86abe5 45920:ddbe94f7242c