# HG changeset patch
# User wenzelm
# Date 1412709078 -7200
# Node ID 4257a7f2bf397cc5d48969e951cc9c0ee71daa73
# Parent  c38d8f139bbcc4302949cbf785f21ff981a0ed34
more cartouches;

diff -r c38d8f139bbc -r 4257a7f2bf39 src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Tue Oct 07 21:01:31 2014 +0200
+++ b/src/HOL/ex/ML.thy	Tue Oct 07 21:11:18 2014 +0200
@@ -2,15 +2,15 @@
     Author:     Makarius
 *)
 
-header {* Isabelle/ML basics *}
+header \<open>Isabelle/ML basics\<close>
 
 theory "ML"
 imports Main
 begin
 
-section {* ML expressions *}
+section \<open>ML expressions\<close>
 
-text {*
+text \<open>
   The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
   text. It is type-checked, compiled, and run within that environment.
 
@@ -18,41 +18,37 @@
   global parameters of the run-time environment (rare).
 
   ML top-level bindings are managed within the theory context.
-*}
-
-ML {* 1 + 1 *}
+\<close>
 
-ML {* val a = 1 *}
-ML {* val b = 1 *}
-ML {* val c = a + b *}
+ML \<open>1 + 1\<close>
 
-
-section {* Antiquotations *}
-
-text {* There are some language extensions (via antiquotations), as explained in
-  the "Isabelle/Isar implementation manual", chapter 0. *}
-
-ML {* length [] *}
-ML {* @{assert} (length [] = 0) *}
+ML \<open>val a = 1\<close>
+ML \<open>val b = 1\<close>
+ML \<open>val c = a + b\<close>
 
 
-text {* Formal entities from the surrounding context may be referenced as
-  follows: *}
-
-term "1 + 1"   -- "term within theory source"
+section \<open>Antiquotations\<close>
 
-ML {*
-  @{term "1 + 1"}   (* term as symbolic ML datatype value *)
-*}
+text \<open>There are some language extensions (via antiquotations), as explained in
+  the ``Isabelle/Isar implementation manual'', chapter 0.\<close>
 
-ML {*
-  @{term "1 + (1::int)"}
-*}
+ML \<open>length []\<close>
+ML \<open>@{assert} (length [] = 0)\<close>
 
 
-section {* IDE support *}
+text \<open>Formal entities from the surrounding context may be referenced as
+  follows:\<close>
+
+term "1 + 1"   -- \<open>term within theory source\<close>
+
+ML \<open>@{term "1 + 1"}   (* term as symbolic ML datatype value *)\<close>
 
-text {*
+ML \<open>@{term "1 + (1::int)"}\<close>
+
+
+section \<open>IDE support\<close>
+
+text \<open>
   ML embedded into the Isabelle environment is connected to the Prover IDE.
   Poly/ML provides:
   \begin{itemize}
@@ -60,70 +56,67 @@
     \item markup for defining positions of identifiers
     \item markup for inferred types of sub-expressions
   \end{itemize}
-*}
+\<close>
 
-ML {* fn i => fn list => length list + i *}
+ML \<open>fn i => fn list => length list + i\<close>
 
 
-section {* Example: factorial and ackermann function in Isabelle/ML *}
+section \<open>Example: factorial and ackermann function in Isabelle/ML\<close>
 
-ML {*
+ML \<open>
   fun factorial 0 = 1
     | factorial n = n * factorial (n - 1)
-*}
-
-ML "factorial 42"
-ML "factorial 10000 div factorial 9999"
+\<close>
 
-text {*
-  See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}
-*}
+ML \<open>factorial 42\<close>
+ML \<open>factorial 10000 div factorial 9999\<close>
 
-ML {*
+text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
+
+ML \<open>
   fun ackermann 0 n = n + 1
     | ackermann m 0 = ackermann (m - 1) 1
     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
-*}
+\<close>
 
-ML {* timeit (fn () => ackermann 3 10) *}
+ML \<open>timeit (fn () => ackermann 3 10)\<close>
 
 
-section {* Parallel Isabelle/ML *}
+section \<open>Parallel Isabelle/ML\<close>
 
-text {*
+text \<open>
   Future.fork/join/cancel manage parallel evaluation.
 
   Note that within Isabelle theory documents, the top-level command boundary may
   not be transgressed without special precautions. This is normally managed by
-  the system when performing parallel proof checking. *}
+  the system when performing parallel proof checking.\<close>
 
-ML {*
+ML \<open>
   val x = Future.fork (fn () => ackermann 3 10);
   val y = Future.fork (fn () => ackermann 3 10);
   val z = Future.join x + Future.join y
-*}
+\<close>
 
-text {*
-  The @{ML_structure Par_List} module provides high-level combinators for
-  parallel list operations. *}
+text \<open>The @{ML_structure Par_List} module provides high-level combinators
+  for parallel list operations.\<close>
 
-ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
-ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
+ML \<open>timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10))\<close>
+ML \<open>timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10))\<close>
 
 
-section {* Function specifications in Isabelle/HOL *}
+section \<open>Function specifications in Isabelle/HOL\<close>
 
 fun factorial :: "nat \<Rightarrow> nat"
 where
   "factorial 0 = 1"
 | "factorial (Suc n) = Suc n * factorial n"
 
-term "factorial 4"  -- "symbolic term"
-value "factorial 4"  -- "evaluation via ML code generation in the background"
+term "factorial 4"  -- \<open>symbolic term\<close>
+value "factorial 4"  -- \<open>evaluation via ML code generation in the background\<close>
 
 declare [[ML_source_trace]]
-ML {* @{term "factorial 4"} *}  -- "symbolic term in ML"
-ML {* @{code "factorial"} *}  -- "ML code from function specification"
+ML \<open>@{term "factorial 4"}\<close>  -- \<open>symbolic term in ML\<close>
+ML \<open>@{code "factorial"}\<close>  -- \<open>ML code from function specification\<close>
 
 
 fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
diff -r c38d8f139bbc -r 4257a7f2bf39 src/HOL/ex/Seq.thy
--- a/src/HOL/ex/Seq.thy	Tue Oct 07 21:01:31 2014 +0200
+++ b/src/HOL/ex/Seq.thy	Tue Oct 07 21:11:18 2014 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 *)
 
-header {* Finite sequences *}
+header \<open>Finite sequences\<close>
 
 theory Seq
 imports Main
diff -r c38d8f139bbc -r 4257a7f2bf39 src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy	Tue Oct 07 21:01:31 2014 +0200
+++ b/src/Tools/SML/Examples.thy	Tue Oct 07 21:11:18 2014 +0200
@@ -2,13 +2,13 @@
     Author:     Makarius
 *)
 
-header {* Standard ML within the Isabelle environment *}
+header \<open>Standard ML within the Isabelle environment\<close>
 
 theory Examples
 imports Pure
 begin
 
-text {*
+text \<open>
   Isabelle/ML is a somewhat augmented version of Standard ML, with
   various add-ons that are indispensable for Isabelle development, but
   may cause conflicts with independent projects in plain Standard ML.
@@ -19,34 +19,34 @@
 
   Here is a very basic example that defines the factorial function and
   evaluates it for some arguments.
-*}
+\<close>
 
 SML_file "factorial.sml"
 
-text {*
+text \<open>
   The subsequent example illustrates the use of multiple 'SML_file'
   commands to build larger Standard ML projects.  The toplevel SML
   environment is enriched cumulatively within the theory context of
   Isabelle --- independently of the Isabelle/ML environment.
-*}
+\<close>
 
 SML_file "Example.sig"
 SML_file "Example.sml"
 
 
-text {*
+text \<open>
   Isabelle/ML and SML share a common run-time system, but the static
   environments are separate.  It is possible to exchange toplevel bindings
   via separate commands like this.
-*}
+\<close>
 
-SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
-ML {* f 42 *}
+SML_export \<open>val f = factorial\<close>  -- \<open>re-use factorial from SML environment\<close>
+ML \<open>f 42\<close>
 
-SML_import {* val println = Output.writeln *}
-  -- {* re-use Isabelle/ML channel for SML *}
+SML_import \<open>val println = Output.writeln\<close>
+  -- \<open>re-use Isabelle/ML channel for SML\<close>
 
-SML_import {* val par_map = Par_List.map *}
-  -- {* re-use Isabelle/ML parallel list combinator for SML *}
+SML_import \<open>val par_map = Par_List.map\<close>
+  -- \<open>re-use Isabelle/ML parallel list combinator for SML\<close>
 
 end