no_document use_thys
["~~/src/HOL/ex/Interpretation_with_Defs",
"~~/src/HOL/Library/While_Combinator",
"~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
];
use_thys
["BExp",
"ASM",
"Small_Step",
"Denotation",
"Comp_Rev",
"Poly_Types",
"Sec_Typing",
"Sec_TypingT",
"Def_Ass_Sound_Big",
"Def_Ass_Sound_Small",
"Live",
"Live_True",
"Hoare_Examples",
"VC",
"HoareT",
"Collecting1",
"Collecting_list",
"Abs_Int_Tests",
"Abs_Int1_parity",
"Abs_Int1_const",
"Abs_Int3",
"Abs_Int_ITP/Abs_Int1_parity_ITP",
"Abs_Int_ITP/Abs_Int1_const_ITP",
"Abs_Int_ITP/Abs_Int3_ITP",
"Abs_Int_Den/Abs_Int_den2",
"Procs_Dyn_Vars_Dyn",
"Procs_Stat_Vars_Dyn",
"Procs_Stat_Vars_Stat",
"C_like",
"OO",
"Fold"
];