src/HOL/MicroJava/ROOT.ML

add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
explicit extraction_expand vs. extraction_expand_def attribute;

no_document use_thys ["While_Combinator"];

use_thys ["MicroJava"];