# HG changeset patch
# User wenzelm
# Date 1222693142 -7200
# Node ID e26aac53723dcbd5f13f933095ecd417a2a65853
# Parent  f9db1da584aca92a1e62588e9140354803af438a
code example: back to individual ML commands, which are now thread-safe;

diff -r f9db1da584ac -r e26aac53723d src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Sep 29 14:41:25 2008 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Sep 29 14:59:02 2008 +0200
@@ -123,61 +123,59 @@
   exec = exec
   test = test
 
-ML {*
-JVM.test;
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-JVM.exec (JVM.E, JVM.the it);
-*}
+ML {* JVM.test *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
+ML {* JVM.exec (JVM.E, JVM.the it) *}
 
 end