--- a/src/Pure/Thy/context.ML Wed May 13 19:06:14 1998 +0200
+++ b/src/Pure/Thy/context.ML Wed May 13 19:06:57 1998 +0200
@@ -22,6 +22,7 @@
signature CONTEXT =
sig
include BASIC_CONTEXT
+ val welcome: unit -> string
val >> : (theory -> theory) -> unit
end;
@@ -37,6 +38,11 @@
fun add_session s = current_session := ! current_session @ [s];
fun reset_session () = current_session := [];
+fun welcome () =
+ "Welcome to Isabelle/" ^
+ (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^
+ " (" ^ version ^ ")";
+
(** theory context **)