# HG changeset patch
# User wenzelm
# Date 1413834483 -7200
# Node ID cee57ab1f76f367dcc726a4774a9919a45d71f45
# Parent  9402a7f15ed55b7c6e44bedc0dcc18b03852ec05
more accurate approximation of AST;

diff -r 9402a7f15ed5 -r cee57ab1f76f src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 20 21:44:33 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 20 21:48:03 2014 +0200
@@ -1588,7 +1588,7 @@
   @{text "('a, 'b)ty"} & @{verbatim "(ty 'a 'b)"} \\
   @{text "\<lambda>x y z. t"} & @{verbatim \<open>("_abs" x ("_abs" y ("_abs" z t)))\<close>} \\
   @{text "\<lambda>x :: 'a. t"} & @{verbatim \<open>("_abs" ("_constrain" x 'a) t)\<close>} \\
-  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim \<open>("==>" P ("==>" Q ("==>" R S)))\<close>} \\
+  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim \<open>("Pure.imp" P ("Pure.imp" Q ("Pure.imp" R S)))\<close>} \\
    @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim \<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close>} \\
   \end{tabular}
   \end{center}