section ‹Basic Declarations› theory IMP2_Basic_Decls imports IMP2_Basic_Simpset begin text ‹Some declarations that are used at several places, and have been factored out.› named_theorems analysis_unfolds ‹Unfold theorems to be applied prior to program analysis functions› named_theorems vcg_preprocess_rules ‹Rules to be applied to goal before VCG› named_theorems vcg_specs ‹Specifications declared to VCG› end