# HG changeset patch
# User wenzelm
# Date 1418235961 -3600
# Node ID 7b1931111e375c28bcfe4be01a88c438d4ad48bb
# Parent  723b11f8ffbf3244db773873073243ae50fb5b97
more examples;

diff -r 723b11f8ffbf -r 7b1931111e37 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Dec 10 19:24:54 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Dec 10 19:26:01 2014 +0100
@@ -261,14 +261,27 @@
   by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
 
 
-subsection \<open>ML syntax: input source\<close>
+subsection \<open>ML syntax\<close>
 
+text \<open>Input source with position information:\<close>
 ML \<open>
   val s: Input.source = \<open>abc\<close>;
-  writeln ("Look here!" ^ Position.here (Input.pos_of s));
+  writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
 
   \<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
     if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
 \<close>
 
+text \<open>Nested ML evaluation:\<close>
+ML \<open>
+  val ML = ML_Context.eval_source ML_Compiler.flags;
+
+  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
+  ML \<open>val b = @{thm sym}\<close>;
+  val c = @{thm trans}
+  val thms = [a, b, c];
+\<close>
+
+ML \<open>\<close>
+
 end