floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
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"
];