src/HOL/IMP/ROOT.ML

IMP compiler with int, added reverse soundness direction

+
−use_thys
+
−["BExp",
+
− "ASM",
+
− "Small_Step",
+
− "Denotation",
+
− "Comp_Rev",
+
− "Poly_Types",
+
− "Sec_Typing",
+
− "Sec_TypingT",
+
− "Def_Ass_Sound_Big",
+
− "Def_Ass_Sound_Small",
+
− "Live",
+
− "Hoare_Examples",
+
− "VC",
+
− "HoareT",
+
− "Procs_Dyn_Vars_Dyn",
+
− "Procs_Stat_Vars_Dyn",
+
− "Procs_Stat_Vars_Stat",
+
− "C_like",
+
− "OO"
+
−];