(* *)+− +− open_file_prelude +− "Tactical_Code.thy"+− (cat_lines ["theory Tactical", +− "imports Base FirstSteps", +− "begin"])+−