src/HOL/MicroJava/J/Decl.ML
changeset 10927 33e290a70445
parent 10925 5ffe7ed8899a