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