# HG changeset patch
# User wenzelm
# Date 1478354831 -3600
# Node ID 73069f272f421e5a56d38070291d01b4c9051e69
# Parent  6f14ce796919f59ed030d813fec0a4ca53494747
documentation of @{undefined} (actually introduced in Isabelle2016);

diff -r 6f14ce796919 -r 73069f272f42 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat Nov 05 14:48:31 2016 +0100
+++ b/src/Doc/Implementation/ML.thy	Sat Nov 05 15:07:11 2016 +0100
@@ -1192,11 +1192,43 @@
 text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
+  @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
   \end{matharray}
 
   \<^descr> \<open>@{assert}\<close> inlines a function @{ML_type "bool -> unit"} that raises @{ML
   Fail} if the argument is @{ML false}. Due to inlining the source position of
   failed assertions is included in the error output.
+
+  \<^descr> \<open>@{undefined}\<close> inlines @{verbatim raise}~@{ML Match}, i.e.\ the ML program
+  behaves as in some function application of an undefined case.
+\<close>
+
+text %mlex \<open>
+  The ML function @{ML undefined} is defined in \<^file>\<open>~~/src/Pure/library.ML\<close>
+  as follows:
+\<close>
+
+ML \<open>fun undefined _ = raise Match\<close>
+
+text \<open>
+  \<^medskip>
+  The following variant uses the antiquotation @{ML_antiquotation undefined}
+  instead:
+\<close>
+
+ML \<open>fun undefined _ = @{undefined}\<close>
+
+text \<open>
+  \<^medskip>
+  Here is the same, using control-symbol notation for the antiquotation, with
+  special rendering of \<^verbatim>\<open>\<^undefined>\<close>:
+\<close>
+
+ML \<open>fun undefined _ = \<^undefined>\<close>
+
+text \<open>
+  \medskip Semantically, all forms are equivalent to a function definition
+  without any clauses, but that is syntactically not allowed in ML.
 \<close>