--- 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"
--- 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
--- 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