# HG changeset patch
# User blanchet
# Date 1448885772 -3600
# Node ID 21c2b1f691d1756ec8cac37c0ba3e6380ae90bd8
# Parent  6af17b2b773d33a60f4526e3b9b39a3b09b9de82
avoid 'hence' and 'thus' in generated proofs

diff -r 6af17b2b773d -r 21c2b1f691d1 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Nov 30 13:14:56 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Nov 30 13:16:12 2015 +0100
@@ -289,7 +289,7 @@
        else "") ^ "obtain"
 
     fun of_show_have qs = if member (op =) qs Show then "show" else "have"
-    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
+    fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have"
 
     fun of_have qs nr =
       if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
@@ -310,8 +310,8 @@
 
     (* Local facts are always passed via "using", which affects "meson" and "metis". This is
        arguably stylistically superior, because it emphasises the structure of the proof. It is also
-       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
-       and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
+       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then"
+       is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
     fun of_method ls ss meth =
       let val direct = is_proof_method_direct meth in
         using_facts ls (if direct then [] else ss) ^