Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
code example: back to individual ML commands, which are now thread-safe;
authorwenzelm
Mon, 29 Sep 2008 14:59:02 +0200
changeset 28408 e26aac53723d
parent 28407 f9db1da584ac
child 28409 a1feb819b0a2
code example: back to individual ML commands, which are now thread-safe;
src/HOL/MicroJava/JVM/JVMListExample.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle