clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
theory MicroJava
imports
"J/JTypeSafe"
"J/Example"
"J/JListExample"
"JVM/JVMListExample"
"JVM/JVMDefensive"
"BV/LBVJVM"
"BV/BVNoTypeError"
"BV/BVExample"
"Comp/CorrComp"
"Comp/CorrCompTp"
begin
end