# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1474556197 -3600
# Node ID d4b89572ae718d1e6e112a619169321fa4a2bf4f
# Parent  f6ce08859d4c015a71dae3e5ba4e59f629960d27# Parent  45ed7d0aeb6fdc5d46858506b04e23876a34cd58
Merge

diff -r f6ce08859d4c -r d4b89572ae71 NEWS
--- a/NEWS	Thu Sep 22 15:44:47 2016 +0100
+++ b/NEWS	Thu Sep 22 15:56:37 2016 +0100
@@ -30,6 +30,15 @@
 to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
 is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
 
+* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> --
+this allows special forms of document output.
+
+* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control
+symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its
+derivatives.
+
+* \<^raw:...> symbols are no longer supported.
+
 * New symbol \<circle>, e.g. for temporal operator.
 
 * Old 'header' command is no longer supported (legacy since
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Implementation/ML.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -1217,13 +1217,6 @@
 
     \<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
 
-    \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of
-    printable characters excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
-    ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
-
-    \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
-    of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
-
   The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
   \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
   symbols and control symbols, but a fixed collection of standard symbols is
@@ -1275,7 +1268,7 @@
   \<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the
   different kinds of symbols explicitly, with constructors @{ML
   "Symbol.Char"}, @{ML "Symbol.UTF8"}, @{ML "Symbol.Sym"}, @{ML
-  "Symbol.Control"}, @{ML "Symbol.Raw"}, @{ML "Symbol.Malformed"}.
+  "Symbol.Control"}, @{ML "Symbol.Malformed"}.
 
   \<^descr> @{ML "Symbol.decode"} converts the string representation of a symbol into
   the datatype version.
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -329,20 +329,21 @@
   printing, notably spaces, blocks, and breaks. The general template format is
   a sequence over any of the following entities.
 
-  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
-  the following special characters:
-
-  \<^medskip>
-  \begin{tabular}{ll}
-    \<^verbatim>\<open>'\<close> & single quote \\
-    \<^verbatim>\<open>_\<close> & underscore \\
-    \<open>\<index>\<close> & index symbol \\
-    \<^verbatim>\<open>(\<close> & open parenthesis \\
-    \<^verbatim>\<open>)\<close> & close parenthesis \\
-    \<^verbatim>\<open>/\<close> & slash \\
-    \<open>\<open> \<close>\<close> & cartouche delimiters \\
-  \end{tabular}
-  \<^medskip>
+  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence delimiter items of the
+  following form:
+    \<^enum> a control symbol followed by a cartouche
+    \<^enum> a single symbol, excluding the following special characters:
+      \<^medskip>
+      \begin{tabular}{ll}
+        \<^verbatim>\<open>'\<close> & single quote \\
+        \<^verbatim>\<open>_\<close> & underscore \\
+        \<open>\<index>\<close> & index symbol \\
+        \<^verbatim>\<open>(\<close> & open parenthesis \\
+        \<^verbatim>\<open>)\<close> & close parenthesis \\
+        \<^verbatim>\<open>/\<close> & slash \\
+        \<open>\<open> \<close>\<close> & cartouche delimiters \\
+      \end{tabular}
+      \<^medskip>
 
   \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
   literal version of the following character, unless that is a blank.
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -229,7 +229,7 @@
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
 @{term "Pair a b"} & @{term[source]"Pair a b"}\\
 @{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term "A \<times> B"} &  \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
+@{term "A \<times> B"} &  \<open>Sigma A (\<lambda>\<^latex>\<open>\_\<close>. B)\<close>
 \end{tabular}
 
 Pairs may be nested. Nesting to the right is printed as a tuple,
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -69,7 +69,7 @@
 Because both subgoals are easy, Isabelle can do it.
 The base case @{prop"add 0 0 = 0"} holds by definition of @{const add},
 and the induction step is almost as simple:
-@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"}
+@{text"add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m"}
 using first the definition of @{const add} and then the induction hypothesis.
 In summary, both subproofs rely on simplification with function definitions and
 the induction hypothesis.
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/LaTeXsugar.thy
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -9,38 +9,38 @@
 begin
 
 (* DUMMY *)
-consts DUMMY :: 'a ("\<^raw:\_>")
+consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
 
 (* THEOREMS *)
 notation (Rule output)
-  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
 syntax (Rule output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
 
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
 
 notation (Axiom output)
-  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
 notation (IfThen output)
-  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
 syntax (IfThen output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
 
 notation (IfThenNoBox output)
-  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
 syntax (IfThenNoBox output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
 setup{*
diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/Logic.thy
--- a/src/Doc/Prog_Prove/Logic.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -340,7 +340,7 @@
 The expression @{text"conjI[of \"a=b\" \"False\"]"}
 instantiates the unknowns in @{thm[source] conjI} from left to right with the
 two formulas @{text"a=b"} and @{text False}, yielding the rule
-@{thm[display,mode=Rule]conjI[of "a=b" False]}
+@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]}
 
 In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates
 the unknowns in the theorem @{text th} from left to right with the terms
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -2863,29 +2863,6 @@
     interpret_floatarith_divide interpret_floatarith_diff
   by auto
 
-lemma interpret_floatarith_tan:
-  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs =
-     tan (interpret_floatarith a vs)"
-  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
-  by auto
-
-lemma interpret_floatarith_log:
-  "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs =
-    log (interpret_floatarith b vs) (interpret_floatarith x vs)"
-  unfolding log_def interpret_floatarith.simps divide_inverse ..
-
-lemma interpret_floatarith_num:
-  shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
-    and "interpret_floatarith (Num (Float 1 0)) vs = 1"
-    and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1"
-    and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a"
-    and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a"
-  by auto
-
-lemma interpret_floatarith_ceiling:
-  "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)"
-  unfolding ceiling_def interpret_floatarith.simps of_int_minus ..
-
 
 subsection "Implement approximation function"
 
@@ -4289,10 +4266,6 @@
 
 subsection \<open>Implement proof method \texttt{approximation}\<close>
 
-lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
-  interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
-  interpret_floatarith_sin interpret_floatarith_ceiling
-
 oracle approximation_oracle = \<open>fn (thy, t) =>
 let
   fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
@@ -4400,6 +4373,61 @@
 lemma meta_eqE: "x \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by auto
 
+named_theorems approximation_preproc
+
+lemma approximation_preproc_floatarith[approximation_preproc]:
+  "0 = real_of_float 0"
+  "1 = real_of_float 1"
+  "0 = Float 0 0"
+  "1 = Float 1 0"
+  "numeral a = Float (numeral a) 0"
+  "numeral a = real_of_float (numeral a)"
+  "x - y = x + - y"
+  "x / y = x * inverse y"
+  "ceiling x = - floor (- x)"
+  "log x y = ln y * inverse (ln x)"
+  "sin x = cos (pi / 2 - x)"
+  "tan x = sin x / cos x"
+  by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq)
+
+lemma approximation_preproc_int[approximation_preproc]:
+  "real_of_int 0 = real_of_float 0"
+  "real_of_int 1 = real_of_float 1"
+  "real_of_int (i + j) = real_of_int i + real_of_int j"
+  "real_of_int (- i) = - real_of_int i"
+  "real_of_int (i - j) = real_of_int i - real_of_int j"
+  "real_of_int (i * j) = real_of_int i * real_of_int j"
+  "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))"
+  "real_of_int (min i j) = min (real_of_int i) (real_of_int j)"
+  "real_of_int (max i j) = max (real_of_int i) (real_of_int j)"
+  "real_of_int (abs i) = abs (real_of_int i)"
+  "real_of_int (i ^ n) = (real_of_int i) ^ n"
+  "real_of_int (numeral a) = real_of_float (numeral a)"
+  "i mod j = i - i div j * j"
+  "i = j \<longleftrightarrow> real_of_int i = real_of_int j"
+  "i \<le> j \<longleftrightarrow> real_of_int i \<le> real_of_int j"
+  "i < j \<longleftrightarrow> real_of_int i < real_of_int j"
+  "i \<in> {j .. k} \<longleftrightarrow> real_of_int i \<in> {real_of_int j .. real_of_int k}"
+  by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality')
+
+lemma approximation_preproc_nat[approximation_preproc]:
+  "real 0 = real_of_float 0"
+  "real 1 = real_of_float 1"
+  "real (i + j) = real i + real j"
+  "real (i - j) = max (real i - real j) 0"
+  "real (i * j) = real i * real j"
+  "real (i div j) = real_of_int (floor (real i / real j))"
+  "real (min i j) = min (real i) (real j)"
+  "real (max i j) = max (real i) (real j)"
+  "real (i ^ n) = (real i) ^ n"
+  "real (numeral a) = real_of_float (numeral a)"
+  "i mod j = i - i div j * j"
+  "n = m \<longleftrightarrow> real n = real m"
+  "n \<le> m \<longleftrightarrow> real n \<le> real m"
+  "n < m \<longleftrightarrow> real n < real m"
+  "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
+  by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality')
+
 ML_file "approximation.ML"
 
 method_setup approximation = \<open>
@@ -4421,6 +4449,17 @@
 
 section "Quickcheck Generator"
 
+lemma approximation_preproc_push_neg[approximation_preproc]:
+  fixes a b::real
+  shows
+    "\<not> (a < b) \<longleftrightarrow> b \<le> a"
+    "\<not> (a \<le> b) \<longleftrightarrow> b < a"
+    "\<not> (a = b) \<longleftrightarrow> b < a \<or> a < b"
+    "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
+    "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
+    "\<not> \<not> q \<longleftrightarrow> q"
+  by auto
+
 ML_file "approximation_generator.ML"
 setup "Approximation_Generator.setup"
 
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -4,6 +4,7 @@
 
 signature APPROXIMATION =
 sig
+  val reify_form: Proof.context -> term -> term
   val approx: int -> Proof.context -> term -> term
   val approximate: Proof.context -> term -> term
   val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic
@@ -54,13 +55,12 @@
     (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
   THEN' resolve_tac ctxt [TrueI]
 
-val form_equations = @{thms interpret_form_equations};
-
 fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
-    fun lookup_splitting (Free (name, _))
-      = case AList.lookup (op =) splitting name
-        of SOME s => HOLogic.mk_number @{typ nat} s
-         | NONE => @{term "0 :: nat"}
+    fun lookup_splitting (Free (name, _)) =
+        (case AList.lookup (op =) splitting name
+          of SOME s => HOLogic.mk_number @{typ nat} s
+           | NONE => @{term "0 :: nat"})
+      | lookup_splitting t = raise TERM ("lookup_splitting", [t])
     val vs = nth (Thm.prems_of st) (i - 1)
              |> Logic.strip_imp_concl
              |> HOLogic.dest_Trueprop
@@ -117,9 +117,13 @@
 fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
 
+fun dest_interpret_env (@{const "interpret_form"} $ _ $ xs) = xs
+  | dest_interpret_env (@{const "interpret_floatarith"} $ _ $ xs) = xs
+  | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
 
-fun dest_float (@{const "Float"} $ m $ e) =
-  (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+  | dest_float t = raise TERM ("dest_float", [t])
+
 
 fun dest_ivl (Const (@{const_name "Some"}, _) $
               (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
@@ -138,8 +142,8 @@
   let
     val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
 
-    fun frac c p 0 digits cnt = (digits, cnt, 0)
-      | frac c 0 r digits cnt = (digits, cnt, r)
+    fun frac _ _ 0 digits cnt = (digits, cnt, 0)
+      | frac _ 0 r digits cnt = (digits, cnt, r)
       | frac c p r digits cnt = (let
         val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
       in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
@@ -190,21 +194,52 @@
   |> SINGLE tactic
   |> the |> Thm.prems_of |> hd
 
-fun prepare_form ctxt term = apply_tactic ctxt term (
-    REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
-      eresolve_tac ctxt @{thms meta_eqE},
-      resolve_tac ctxt @{thms impI}] 1)
-    THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1
-    THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1)))
+fun preproc_form_conv ctxt =
+  Simplifier.rewrite
+   (put_simpset HOL_basic_ss ctxt addsimps
+     (Named_Theorems.get ctxt @{named_theorems approximation_preproc}))
+
+fun reify_form_conv ctxt ct =
+  let
+    val thm =
+       Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps} ct
+       handle ERROR msg =>
+        cat_error ("Reification failed: " ^ msg)
+          ("Approximation does not support " ^
+            quote (Syntax.string_of_term ctxt (Thm.term_of ct)))
+    fun check_env (Free _) = ()
+      | check_env (Var _) = ()
+      | check_env t =
+          cat_error "Term not supported by approximation:" (Syntax.string_of_term ctxt t)
+    val _ = Thm.rhs_of thm |> Thm.term_of |> dest_interpret_env |> HOLogic.dest_list |> map check_env
+  in thm end
 
-fun reify_form ctxt term = apply_tactic ctxt term
-   (Reification.tac ctxt form_equations NONE 1)
+
+fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i
+
+fun prepare_form_tac ctxt i =
+  REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
+    eresolve_tac ctxt @{thms meta_eqE},
+    resolve_tac ctxt @{thms impI}] i)
+  THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
+  THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
+  THEN CONVERSION (Conv.arg_conv (preproc_form_conv ctxt)) i
+
+fun prepare_form ctxt term = apply_tactic ctxt term (prepare_form_tac ctxt 1)
+
+fun apply_reify_form ctxt t = apply_tactic ctxt t (reify_form_tac ctxt 1)
+
+fun reify_form ctxt t = HOLogic.mk_Trueprop t
+  |> prepare_form ctxt
+  |> apply_reify_form ctxt
+  |> HOLogic.dest_Trueprop
 
 fun approx_form prec ctxt t =
         realify t
      |> prepare_form ctxt
-     |> (fn arith_term => reify_form ctxt arith_term
-         |> HOLogic.dest_Trueprop |> dest_interpret_form
+     |> (fn arith_term => apply_reify_form ctxt arith_term
+         |> HOLogic.dest_Trueprop
+         |> dest_interpret_form
          |> (fn (data, xs) =>
             mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
               (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
@@ -216,7 +251,7 @@
 
 fun approx_arith prec ctxt t = realify t
      |> Thm.cterm_of ctxt
-     |> Reification.conv ctxt form_equations
+     |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt)
      |> Thm.prop_of
      |> Logic.dest_equals |> snd
      |> dest_interpret |> fst
@@ -252,13 +287,9 @@
       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
 
 fun approximation_tac prec splitting taylor ctxt i =
-  REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE},
-                  eresolve_tac ctxt @{thms meta_eqE},
-                  resolve_tac ctxt @{thms impI}] i)
-  THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i
-  THEN DETERM (TRY (filter_prems_tac ctxt (K false) i))
-  THEN DETERM (Reification.tac ctxt form_equations NONE i)
+  prepare_form_tac ctxt i
+  THEN reify_form_tac ctxt i
   THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
   THEN gen_eval_tac (approximation_conv ctxt) ctxt i
-    
+
 end;
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/approximation_generator.ML
--- a/src/HOL/Decision_Procs/approximation_generator.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -55,6 +55,7 @@
   | mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
   | mapprox_floatarith (@{term Power} $ a $ n) xs =
       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
+  | mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
   | mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n)
   | mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m
   | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
@@ -130,7 +131,13 @@
           (map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $
         @{term "[] :: nat list"}
   in
-    (if mapprox_form eps e (map (real_of_Float o fst) rs)
+    (if
+      mapprox_form eps e (map (real_of_Float o fst) rs)
+      handle
+        General.Overflow => false
+      | General.Domain => false
+      | General.Div => false
+      | IEEEReal.Unordered => false
     then
       let
         val ts = map (fn x => snd x ()) rs
@@ -154,19 +161,12 @@
     "a = b \<longleftrightarrow> a \<le> b \<and> b \<le> a"
     "(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q"
     "(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)"
-    "\<not> (a < b) \<longleftrightarrow> b \<le> a"
-    "\<not> (a \<le> b) \<longleftrightarrow> b < a"
-    "\<not> (p \<and> q) \<longleftrightarrow> \<not> p \<or> \<not> q"
-    "\<not> (p \<or> q) \<longleftrightarrow> \<not> p \<and> \<not> q"
-    "\<not> \<not> q \<longleftrightarrow> q"
     by auto}
 
-val form_equations = @{thms interpret_form_equations};
-
 fun reify_goal ctxt t =
   HOLogic.mk_not t
     |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
-    |> conv_term ctxt (Reification.conv ctxt form_equations)
+    |> Approximation.reify_form ctxt
     |> dest_interpret_form
     ||> HOLogic.dest_list
 
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -78,6 +78,10 @@
 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x"
   by (approximation 30 splitting: x=1 taylor: x = 3)
 
-approximate "10"
+lemma "(n::real) \<in> {32 .. 62} \<Longrightarrow> \<lceil>log 2 (2 * (\<lfloor>n\<rfloor> div 2) + 1)\<rceil> = \<lceil>log 2 (\<lfloor>n\<rfloor> + 1)\<rceil>"
+  unfolding eq_iff
+  by (approximation 20)
+
+approximate 10
 
 end
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -10,15 +10,15 @@
 
 (* LOGIC *)
 notation (latex output)
-  If  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
+  If  ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)
 
 syntax (latex output)
 
   "_Let"        :: "[letbinds, 'a] => 'a"
-  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
+  ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
 
   "_case_syntax":: "['a, cases_syn] => 'b"
-  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
+  ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
 
 
 (* SETS *)
@@ -59,41 +59,41 @@
 
 (* nth *)
 notation (latex output)
-  nth  ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000)
+  nth  ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
 
 (* DUMMY *)
-consts DUMMY :: 'a ("\<^raw:\_>")
+consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
 
 (* THEOREMS *)
 notation (Rule output)
-  Pure.imp  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
 syntax (Rule output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
 
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
 
 notation (Axiom output)
-  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
 
 notation (IfThen output)
-  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
 syntax (IfThen output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
 
 notation (IfThenNoBox output)
-  Pure.imp  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
 syntax (IfThenNoBox output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
 setup\<open>
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -27,7 +27,7 @@
 
 (* append *)
 syntax (latex output)
-  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+  "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
 translations
   "_appendL xs ys" <= "xs @ ys" 
   "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
@@ -36,8 +36,8 @@
 (* deprecated, use thm with style instead, will be removed *)
 (* aligning equations *)
 notation (tab output)
-  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
-  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+  "HOL.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
+  "Pure.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
 
 (* Let *)
 translations 
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Sep 22 15:56:37 2016 +0100
@@ -1609,13 +1609,13 @@
 
 syntax (latex_sum output)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
   "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
   "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
 
 syntax
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
@@ -2013,13 +2013,13 @@
 
 syntax (latex_prod output)
   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
   "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
   "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
+ ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
 
 syntax
   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -125,8 +125,8 @@
     val get = maps (Proof_Context.get_fact ctxt o fst)
     val keywords = Thy_Header.get_keywords' ctxt
   in
-    Source.of_string name
-    |> Symbol.source
+    Symbol.explode name
+    |> Source.of_list
     |> Token.source keywords Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse.thms1 >> get)
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/General/symbol.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -1,5 +1,5 @@
 (*  Title:      Pure/General/symbol.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Generalized characters with infinitely many named symbols.
 *)
@@ -7,6 +7,7 @@
 signature SYMBOL =
 sig
   type symbol = string
+  val explode: string -> symbol list
   val spaces: int -> string
   val STX: symbol
   val DEL: symbol
@@ -41,12 +42,8 @@
   val to_ascii_upper: symbol -> symbol
   val is_ascii_identifier: string -> bool
   val scan_ascii_id: string list -> string * string list
-  val is_raw: symbol -> bool
-  val decode_raw: symbol -> string
-  val encode_raw: string -> string
   datatype sym =
-    Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
-    Malformed of string | EOF
+    Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
   val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
@@ -58,8 +55,6 @@
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val beginning: int -> symbol list -> string
-  val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
-  val explode: string -> symbol list
   val esc: symbol -> string
   val escape: string -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
@@ -81,11 +76,10 @@
 (*Symbols, which are considered the smallest entities of any Isabelle
   string, may be of the following form:
 
-    (1) ASCII symbols: a
+    (1) ASCII: a
+    (2) UTF-8: ä
     (2) regular symbols: \<ident>
     (3) control symbols: \<^ident>
-    (4) raw control symbols: \<^raw:...>, where "..." may be any printable
-        character (excluding ".", ">"), or \<^raw000>
 
   Output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools.
@@ -191,31 +185,6 @@
 val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
 
 
-(* encode_raw *)
-
-fun raw_chr c =
-  is_char c andalso
-    (ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
-      orelse ord c >= 128);
-
-fun encode_raw "" = ""
-  | encode_raw str =
-      let
-        val raw0 = enclose "\092<^raw:" ">";
-        val raw1 = raw0 o implode;
-        val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;
-
-        fun encode cs = enc (take_prefix raw_chr cs)
-        and enc ([], []) = []
-          | enc (cs, []) = [raw1 cs]
-          | enc ([], d :: ds) = raw2 d :: encode ds
-          | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
-      in
-        if exists_string (not o raw_chr) str then implode (encode (raw_explode str))
-        else raw0 str
-      end;
-
-
 (* diagnostics *)
 
 fun beginning n cs =
@@ -230,28 +199,15 @@
   end;
 
 
-(* decode_raw *)
-
-fun is_raw s =
-  String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s;
-
-fun decode_raw s =
-  if not (is_raw s) then error (malformed_msg s)
-  else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
-  else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
-
-
 (* symbol variants *)
 
 datatype sym =
-  Char of string | UTF8 of string | Sym of string | Control of string | Raw of string |
-  Malformed of string | EOF;
+  Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF;
 
 fun decode s =
   if s = "" then EOF
   else if is_char s then Char s
   else if is_utf8 s then UTF8 s
-  else if is_raw s then Raw (decode_raw s)
   else if is_malformed s then Malformed s
   else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
@@ -429,65 +385,6 @@
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 
 
-
-(** symbol input **)
-
-(* source *)
-
-local
-
-fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";
-
-fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
-
-fun implode_pseudo_utf8 (cs as ["\192", c]) =
-      if ord c < 160 then chr (ord c - 128) else implode cs
-  | implode_pseudo_utf8 cs = implode cs;
-
-val scan_encoded_newline =
-  $$ "\^M" -- $$ "\n" >> K "\n" ||
-  $$ "\^M" >> K "\n";
-
-val scan_raw =
-  Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
-  Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
-
-val scan_total =
-  Scan.one is_plain ||
-  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
-  scan_encoded_newline ||
-  ($$ "\\" ^^ $$ "<" ^^
-    (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
-      Scan.optional ($$ ">") "")) ||
-  Scan.one not_eof;
-
-in
-
-fun source src = Source.source stopper (Scan.bulk scan_total) src;
-
-end;
-
-
-(* explode *)
-
-local
-
-fun no_explode [] = true
-  | no_explode ("\\" :: "<" :: _) = false
-  | no_explode ("\^M" :: _) = false
-  | no_explode (c :: cs) = is_ascii c andalso no_explode cs;
-
-in
-
-fun sym_explode str =
-  let val chs = raw_explode str in
-    if no_explode chs then chs
-    else Source.exhaust (source (Source.of_list chs))
-  end;
-
-end;
-
-
 (* escape *)
 
 val esc = fn s =>
@@ -495,7 +392,7 @@
   else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
   else "\\" ^ s;
 
-val escape = implode o map esc o sym_explode;
+val escape = implode o map esc o Symbol.explode;
 
 
 
@@ -523,12 +420,12 @@
 
 val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
 
-val explode_words = split_words o sym_explode;
+val explode_words = split_words o Symbol.explode;
 
 
 (* blanks *)
 
-val trim_blanks = sym_explode #> trim is_blank #> implode;
+val trim_blanks = Symbol.explode #> trim is_blank #> implode;
 
 
 (* bump string -- treat as base 26 or base 1 numbers *)
@@ -539,7 +436,7 @@
   | symbolic_end [] = false;
 
 fun bump_init str =
-  if symbolic_end (rev (sym_explode str)) then str ^ "'"
+  if symbolic_end (rev (Symbol.explode str)) then str ^ "'"
   else str ^ "a";
 
 fun bump_string str =
@@ -551,7 +448,7 @@
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
-    val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));
+    val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;
 
@@ -574,11 +471,11 @@
 
 val xsymbolsN = "xsymbols";
 
-fun output s = (s, sym_length (sym_explode s));
+fun output s = (s, sym_length (Symbol.explode s));
 
 
 (*final declarations of this structure!*)
-val explode = sym_explode;
+val explode = Symbol.explode;
 val length = sym_length;
 
 end;
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/General/symbol.scala	Thu Sep 22 15:56:37 2016 +0100
@@ -64,9 +64,7 @@
   /* symbol matching */
 
   private val symbol_total = new Regex("""(?xs)
-    [\ud800-\udbff][\udc00-\udfff] | \r\n |
-    \\ < (?: \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* | \^? ([A-Za-z][A-Za-z0-9_']*)? ) >? |
-    .""")
+    [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""")
 
   private def is_plain(c: Char): Boolean =
     !(c == '\r' || c == '\\' || Character.isHighSurrogate(c))
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol_explode.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/symbol_explode.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -0,0 +1,53 @@
+(*  Title:      Pure/General/symbol_explode.ML
+    Author:     Makarius
+
+String explode operation for Isabelle symbols (see also symbol.ML).
+*)
+
+structure Symbol: sig val explode: string -> string list end =
+struct
+
+fun is_ascii_letter c = #"A" <= c andalso c <= #"Z" orelse #"a" <= c andalso c <= #"z";
+fun is_ascii_letdig c =
+  is_ascii_letter c orelse #"0" <= c andalso c <= #"9" orelse c = #"_" orelse c = #"'";
+
+fun is_utf8 c = c >= #"\128";
+fun is_utf8_trailer c = #"\128" <= c andalso c < #"\192";
+fun is_utf8_control c = #"\128" <= c andalso c < #"\160";
+
+fun explode string =
+  let
+    fun char i = String.sub (string, i);
+    fun string_range i j = String.substring (string, i, j - i);
+
+    val n = size string;
+    fun test pred i = i < n andalso pred (char i);
+    fun many pred i = if test pred i then many pred (i + 1) else i;
+    fun maybe pred i = if test pred i then i + 1 else i;
+    fun maybe_char c = maybe (fn c' => c = c');
+    fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;
+
+    fun scan i =
+      if i < n then
+        let val ch = char i in
+          (*encoded newline*)
+          if ch = #"\^M" then "\n" :: scan (maybe_char #"\n" (i + 1))
+          (*pseudo utf8: encoded ascii control*)
+          else if ch = #"\192" andalso
+            test is_utf8_control (i + 1) andalso not (test is_utf8 (i + 2))
+          then chr (Char.ord (char (i + 1)) - 128) :: scan (i + 2)
+          (*utf8*)
+          else if is_utf8 ch then
+            let val j = many is_utf8_trailer (i + 1)
+            in string_range i j :: scan j end
+          (*named symbol*)
+          else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
+            let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
+            in string_range i j :: scan j end
+          (*single character*)
+          else String.str ch :: scan (i + 1)
+        end
+      else [];
+  in scan 0 end;
+
+end;
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -220,17 +220,17 @@
 
 in
 
-fun parse thy pos str =
-  Source.of_string str
-  |> Symbol.source
-  |> Token.source (Thy_Header.get_keywords thy) pos
-  |> commands_source thy
-  |> Source.exhaust;
+fun parse thy pos =
+  Symbol.explode
+  #> Source.of_list
+  #> Token.source (Thy_Header.get_keywords thy) pos
+  #> commands_source thy
+  #> Source.exhaust;
 
-fun parse_tokens thy toks =
-  Source.of_list toks
-  |> commands_source thy
-  |> Source.exhaust;
+fun parse_tokens thy =
+  Source.of_list
+  #> commands_source thy
+  #> Source.exhaust;
 
 end;
 
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Isar/token.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -650,8 +650,8 @@
 (* explode *)
 
 fun explode keywords pos =
-  Source.of_string #>
-  Symbol.source #>
+  Symbol.explode #>
+  Source.of_list #>
   source keywords pos #>
   Source.exhaust;
 
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/ML/ml_lex.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -351,7 +351,7 @@
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover);
 
-val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
+val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
 
 val read_pos = gen_read false;
 
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -10,6 +10,7 @@
 ML_file "System/distribution.ML";
 
 ML_file "General/basics.ML";
+ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -251,9 +251,10 @@
 
 val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
 
-val scan_delim_char =
-  $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
-  scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
+val scan_delim =
+  scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||
+  $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single ||
+  scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single;
 
 val scan_sym =
   $$ "_" >> K (Argument ("", 0)) ||
@@ -265,7 +266,7 @@
   $$ "/" -- $$ "/" >> K (Brk ~1) ||
   $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) ||
   scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) ||
-  Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
+  Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat);
 
 val scan_symb =
   Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Thy/html.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -48,11 +48,9 @@
 val no_symbols = make_symbols [];
 
 fun output_sym (Symbols tab) s =
-  if Symbol.is_raw s then Symbol.decode_raw s
-  else
-    (case Symtab.lookup tab s of
-      SOME x => x
-    | NONE => XML.text s);
+  (case Symtab.lookup tab s of
+    SOME x => x
+  | NONE => XML.text s);
 
 end;
 
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -7,6 +7,9 @@
 signature LATEX =
 sig
   val output_ascii: string -> string
+  val latex_control: Symbol.symbol
+  val is_latex_control: Symbol.symbol -> bool
+  val embed_raw: string -> string
   val output_known_symbols: (string -> bool) * (string -> bool) ->
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
@@ -41,6 +44,11 @@
 
 (* output symbols *)
 
+val latex_control = "\<^latex>";
+fun is_latex_control s = s = latex_control;
+
+val embed_raw = prefix latex_control o cartouche;
+
 local
 
 val char_table =
@@ -95,13 +103,26 @@
   | Symbol.UTF8 s => s
   | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym
   | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym
-  | Symbol.Raw s => s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
+fun scan_latex known =
+  Scan.one (is_latex_control o Symbol_Pos.symbol) |--
+    Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
+  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
+
+fun read_latex known syms =
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
+      (map (rpair Position.none) syms) of
+    SOME ss => implode ss
+  | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
+
 in
 
-val output_known_symbols = implode oo (map o output_known_sym);
+fun output_known_symbols known syms =
+  if exists is_latex_control syms then read_latex known syms
+  else implode (map (output_known_sym known) syms);
+
 val output_symbols = output_known_symbols (K true, K true);
 val output_syms = output_symbols o Symbol.explode;
 
@@ -192,7 +213,7 @@
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
 
-val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
+val _ = Output.add_mode latexN latex_output embed_raw;
 val _ = Markup.add_mode latexN latex_markup;
 val _ = Pretty.add_mode latexN latex_indent;
 
diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Sep 22 15:44:47 2016 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Sep 22 15:56:37 2016 +0100
@@ -168,11 +168,10 @@
 val header =
   (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
 
-fun token_source pos str =
-  str
-  |> Source.of_string_limited 8000
-  |> Symbol.source
-  |> Token.source_strict bootstrap_keywords pos;
+fun token_source pos =
+  Symbol.explode
+  #> Source.of_list
+  #> Token.source_strict bootstrap_keywords pos;
 
 fun read_source pos source =
   let val res =