# HG changeset patch # User wenzelm # Date 896350925 -7200 # Node ID f14ec8ec1db1c62afe563176a0c72d5627f38685 # Parent 6cec2c0ffdbf4f52ef334dbb16802a8dfe7db86b version under control of Admin/makedist; ml_prompts; diff -r 6cec2c0ffdbf -r f14ec8ec1db1 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu May 28 12:21:05 1998 +0200 +++ b/src/Pure/ROOT.ML Thu May 28 12:22:05 1998 +0200 @@ -8,9 +8,10 @@ *) val banner = "Pure Isabelle"; -val version = "Isabelle98: January 1998"; +val version = "Internal working version of Isabelle"; print_depth 1; +ml_prompts "> " "# "; (*basic utils*)