diff -r cf6bb75968c4 -r 53900a320a87 src/Pure/Thy/context.ML
--- 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 **)