somewhat adhoc replacement for 'thus' and 'hence';
complete words as short as 2 characters, e.g. "Un";

--- a/src/Pure/Isar/outer_syntax.scala	Sat Nov 13 21:46:24 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Nov 13 22:33:07 2010 +0100
@@ -18,11 +18,11 @@
 
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 
-  def + (name: String, kind: String): Outer_Syntax =
+  def + (name: String, kind: String, replace: String): Outer_Syntax =
   {
     val new_keywords = keywords + (name -> kind)
     val new_lexicon = lexicon + name
-    val new_completion = completion + name
+    val new_completion = completion + (name, replace)
     new Outer_Syntax(symbols) {
       override val lexicon = new_lexicon
       override val keywords = new_keywords
@@ -30,6 +30,8 @@
     }
   }
 
+  def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
+
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
 
   def is_command(name: String): Boolean =

--- a/src/Pure/System/session.scala	Sat Nov 13 21:46:24 2010 +0100
+++ b/src/Pure/System/session.scala	Sat Nov 13 22:33:07 2010 +0100
@@ -208,7 +208,12 @@
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
-            if (result.is_ready) phase = Session.Ready
+            if (result.is_ready) {
+              // FIXME move to ML side
+              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
+              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
+              phase = Session.Ready
+            }
             else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
             else if (result.is_exit) phase = Session.Inactive
           }

--- a/src/Pure/Thy/completion.scala	Sat Nov 13 21:46:24 2010 +0100
+++ b/src/Pure/Thy/completion.scala	Sat Nov 13 22:33:07 2010 +0100
@@ -23,7 +23,7 @@
 
     def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
     def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
-    def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
+    def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
 
     def read(in: CharSequence): Option[String] =
     {
@@ -49,17 +49,19 @@
 
   /* adding stuff */
 
-  def + (keyword: String): Completion =
+  def + (keyword: String, replace: String): Completion =
   {
     val old = this
     new Completion {
       override val words_lex = old.words_lex + keyword
-      override val words_map = old.words_map + (keyword -> keyword)
+      override val words_map = old.words_map + (keyword -> replace)
       override val abbrevs_lex = old.abbrevs_lex
       override val abbrevs_map = old.abbrevs_map
     }
   }
 
+  def + (keyword: String): Completion = this + (keyword, keyword)
+
   def + (symbols: Symbol.Interpretation): Completion =
   {
     val words =