
diff -r 3480725c71d2 -r 0debd22f0c0e src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Implementation/Syntax.thy	Tue Oct 20 23:53:40 2015 +0200
@@ -6,7 +6,7 @@
 
 chapter \<open>Concrete syntax and type-checking\<close>
 
-text \<open>Pure @{text "\<lambda>"}-calculus as introduced in \chref{ch:logic} is
+text \<open>Pure \<open>\<lambda>\<close>-calculus as introduced in \chref{ch:logic} is
   an adequate foundation for logical languages --- in the tradition of
   \<^emph>\<open>higher-order abstract syntax\<close> --- but end-users require
   additional means for reading and printing of terms and types.  This
@@ -15,12 +15,11 @@
   the theory and proof language @{cite "isabelle-isar-ref"}.
 
   For example, according to @{cite church40} quantifiers are represented as
-  higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
-  "All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
-  Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
+  higher-order constants \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> such that \<open>All (\<lambda>x::'a. B x)\<close> faithfully represents the idea that is displayed in
+  Isabelle as \<open>\<forall>x::'a. B x\<close> via @{keyword "binder"} notation.
   Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner}
-  (and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
-  the type @{text "'a"} is already clear from the
+  (and extensions) enables users to write \<open>\<forall>x. B x\<close> concisely, when
+  the type \<open>'a\<close> is already clear from the
   context.\footnote{Type-inference taken to the extreme can easily confuse
   users. Beginners often stumble over unexpectedly general types inferred by
   the system.}
@@ -36,22 +35,21 @@
   \secref{sec:term-check}, respectively.  This results in the
   following decomposition of the main operations:
 
-  \<^item> @{text "read = parse; check"}
+  \<^item> \<open>read = parse; check\<close>
 
-  \<^item> @{text "pretty = uncheck; unparse"}
+  \<^item> \<open>pretty = uncheck; unparse\<close>
 
 
   For example, some specification package might thus intercept syntax
-  processing at a well-defined stage after @{text "parse"}, to a augment the
-  resulting pre-term before full type-reconstruction is performed by @{text
-  "check"}. Note that the formal status of bound variables, versus free
+  processing at a well-defined stage after \<open>parse\<close>, to a augment the
+  resulting pre-term before full type-reconstruction is performed by \<open>check\<close>. Note that the formal status of bound variables, versus free
   variables, versus constants must not be changed between these phases.
 
   \<^medskip>
-  In general, @{text check} and @{text uncheck} operate
+  In general, \<open>check\<close> and \<open>uncheck\<close> operate
   simultaneously on a list of terms. This is particular important for
   type-checking, to reconstruct types for several terms of the same context
-  and scope. In contrast, @{text parse} and @{text unparse} operate separately
+  and scope. In contrast, \<open>parse\<close> and \<open>unparse\<close> operate separately
   on single terms.
 
   There are analogous operations to read and print types, with the same
@@ -63,11 +61,10 @@
 
 text \<open>
   Read and print operations are roughly dual to each other, such that for the
-  user @{text "s' = pretty (read s)"} looks similar to the original source
-  text @{text "s"}, but the details depend on many side-conditions. There are
+  user \<open>s' = pretty (read s)\<close> looks similar to the original source
+  text \<open>s\<close>, but the details depend on many side-conditions. There are
   also explicit options to control the removal of type information in the
-  output. The default configuration routinely looses information, so @{text
-  "t' = read (pretty t)"} might fail, or produce a differently typed term, or
+  output. The default configuration routinely looses information, so \<open>t' = read (pretty t)\<close> might fail, or produce a differently typed term, or
   a completely different term in the face of syntactic overloading.
 \<close>
 
@@ -85,10 +82,10 @@
   @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a
+  \<^descr> @{ML Syntax.read_typs}~\<open>ctxt strs\<close> parses and checks a
   simultaneous list of source strings as types of the logic.
 
-  \<^descr> @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a
+  \<^descr> @{ML Syntax.read_terms}~\<open>ctxt strs\<close> parses and checks a
   simultaneous list of source strings as terms of the logic.
   Type-reconstruction puts all parsed terms into the same scope: types of
   free variables ultimately need to coincide.
@@ -98,7 +95,7 @@
   is possible to use @{ML Type.constraint} on the intermediate pre-terms
   (\secref{sec:term-check}).
 
-  \<^descr> @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
+  \<^descr> @{ML Syntax.read_props}~\<open>ctxt strs\<close> parses and checks a
   simultaneous list of source strings as terms of the logic, with an implicit
   type-constraint for each argument to enforce type @{typ prop}; this also
   affects the inner syntax for parsing. The remaining type-reconstruction
@@ -110,8 +107,8 @@
   its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where
   @{ML Syntax.read_terms} is actually intended!
 
-  \<^descr> @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML
-  Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type
+  \<^descr> @{ML Syntax.pretty_typ}~\<open>ctxt T\<close> and @{ML
+  Syntax.pretty_term}~\<open>ctxt t\<close> uncheck and pretty-print the given type
   or term, respectively. Although the uncheck phase acts on a simultaneous
   list as well, this is rarely used in practice, so only the singleton case is
   provided as combined pretty operation. There is no distinction of term vs.\
@@ -173,22 +170,22 @@
   @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as
+  \<^descr> @{ML Syntax.parse_typ}~\<open>ctxt str\<close> parses a source string as
   pre-type that is ready to be used with subsequent check operations.
 
-  \<^descr> @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as
+  \<^descr> @{ML Syntax.parse_term}~\<open>ctxt str\<close> parses a source string as
   pre-term that is ready to be used with subsequent check operations.
 
-  \<^descr> @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as
+  \<^descr> @{ML Syntax.parse_prop}~\<open>ctxt str\<close> parses a source string as
   pre-term that is ready to be used with subsequent check operations. The
   inner syntax category is @{typ prop} and a suitable type-constraint is
   included to ensure that this information is observed in subsequent type
   reconstruction.
 
-  \<^descr> @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after
+  \<^descr> @{ML Syntax.unparse_typ}~\<open>ctxt T\<close> unparses a type after
   uncheck operations, to turn it into a pretty tree.
 
-  \<^descr> @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after
+  \<^descr> @{ML Syntax.unparse_term}~\<open>ctxt T\<close> unparses a term after
   uncheck operations, to turn it into a pretty tree. There is no distinction
   for propositions here.
 
@@ -212,9 +209,8 @@
 
   A typical add-on for the check/uncheck syntax layer is the @{command
   abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies
-  syntactic definitions that are managed by the system as polymorphic @{text
-  "let"} bindings. These are expanded during the @{text "check"} phase, and
-  contracted during the @{text "uncheck"} phase, without affecting the
+  syntactic definitions that are managed by the system as polymorphic \<open>let\<close> bindings. These are expanded during the \<open>check\<close> phase, and
+  contracted during the \<open>uncheck\<close> phase, without affecting the
   type-assignment of the given terms.
 
   \<^medskip>
@@ -222,7 +218,7 @@
   additional check/uncheck modules might be defined in user space.
 
   For example, the @{command class} command defines a context where
-  @{text "check"} treats certain type instances of overloaded
+  \<open>check\<close> treats certain type instances of overloaded
   constants according to the ``dictionary construction'' of its
   logical foundation.  This involves ``type improvement''
   (specialization of slightly too general types) and replacement by
@@ -238,11 +234,11 @@
   @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list
+  \<^descr> @{ML Syntax.check_typs}~\<open>ctxt Ts\<close> checks a simultaneous list
   of pre-types as types of the logic.  Typically, this involves normalization
   of type synonyms.
 
-  \<^descr> @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list
+  \<^descr> @{ML Syntax.check_terms}~\<open>ctxt ts\<close> checks a simultaneous list
   of pre-terms as terms of the logic. Typically, this involves type-inference
   and normalization term abbreviations. The types within the given terms are
   treated in the same way as for @{ML Syntax.check_typs}.
@@ -253,15 +249,15 @@
   is checked; afterwards the type arguments are recovered with @{ML
   Logic.dest_type}.
 
-  \<^descr> @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list
+  \<^descr> @{ML Syntax.check_props}~\<open>ctxt ts\<close> checks a simultaneous list
   of pre-terms as terms of the logic, such that all terms are constrained by
   type @{typ prop}. The remaining check operation works as @{ML
   Syntax.check_terms} above.
 
-  \<^descr> @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous
+  \<^descr> @{ML Syntax.uncheck_typs}~\<open>ctxt Ts\<close> unchecks a simultaneous
   list of types of the logic, in preparation of pretty printing.
 
-  \<^descr> @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous
+  \<^descr> @{ML Syntax.uncheck_terms}~\<open>ctxt ts\<close> unchecks a simultaneous
   list of terms of the logic, in preparation of pretty printing. There is no
   distinction for propositions here.
 




