| changeset 10937 | 5651e0636e38 |
| parent 10571 | fdde440a9033 |
| child 11509 | d54301357129 |
| 10936:a0dc597d9173 | 10937:5651e0636e38 |
|---|---|
30 |
30 |
31 (* access path *) |
31 (* access path *) |
32 |
32 |
33 fun path () = ! session_path; |
33 fun path () = ! session_path; |
34 |
34 |
35 fun str_of [] = "Pure" |
35 fun str_of [] = pure |
36 | str_of elems = space_implode "/" elems; |
36 | str_of elems = space_implode "/" elems; |
37 |
37 |
38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; |
39 |
39 |
40 |
40 |