# HG changeset patch
# User wenzelm
# Date 1379342812 -7200
# Node ID 51595a047730b027af5668dfc77f18ed013bd027
# Parent  62f42e9ec0f301708c7f57f3a22cee0baabd7227
proper Isabelle symbols -- no UTF8 here;

diff -r 62f42e9ec0f3 -r 51595a047730 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 14:21:07 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 16:46:52 2013 +0200
@@ -2,13 +2,13 @@
     Author:     Manuel Eberl, TU Muenchen
 
 Generates the pelims rules for a function. These are of the shape
-[|f x y z = w; !!…. [|x = …; y = …; z = …; w = …|] ==> P; …|] ==> P
+[|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P
 and are derived from the cases rule. There is at least one pelim rule for
 each function (cf. mutually recursive functions)
 There may be more than one pelim rule for a function in case of functions
 that return a boolean. For such a function, e.g. P x, not only the normal
 elim rule with the premise P x = z is generated, but also two additional
-elim rules with P x resp. ¬P x as premises.
+elim rules with P x resp. \<not>P x as premises.
 *)
 
 signature FUNCTION_ELIMS =
diff -r 62f42e9ec0f3 -r 51595a047730 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Sep 16 14:21:07 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Sep 16 16:46:52 2013 +0200
@@ -71,10 +71,10 @@
     val assms = assms |> map (Display.pretty_thm ctxt)
                       |> (fn [] => Pretty.str ""
                            | [a] => a
-                           | assms => Pretty.enum ";" "⟦" "⟧" assms)
+                           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
     val concl = concl |> Syntax.pretty_term ctxt
     val trace_list = [] |> cons concl
-                        |> nr_of_assms>0 ? cons (Pretty.str "⟹")
+                        |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
                         |> cons assms
                         |> cons time
     val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)