(* Scripting buffer for theory A *)