--- 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 =
--- 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)