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