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.
tuned ML declarations;
authorwenzelm
Mon, 30 Jul 2007 19:46:15 +0200
changeset 24074 40f414b87655
parent 24073 373727835757
child 24075 366d4d234814
tuned ML declarations;
src/HOL/MicroJava/Comp/CorrComp.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/J/Example.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/JVM/JVMListExample.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Jul 30 19:46:13 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Jul 30 19:46:15 2007 +0200
@@ -476,9 +476,7 @@
 (* to avoid automatic pair splits *)
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-ML_setup {*
-change_simpset (fn ss => ss delloop "split_all_tac");
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
 
 lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
@@ -1265,9 +1263,7 @@
 
 (* reinstall pair splits *)
 declare split_paired_All [simp] split_paired_Ex [simp]
-ML_setup {*
-change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
-*}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 declare wf_prog_ws_prog [simp del]
 
--- a/src/HOL/MicroJava/J/Example.thy	Mon Jul 30 19:46:13 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Jul 30 19:46:15 2007 +0200
@@ -127,7 +127,8 @@
 abbreviation "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
 abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
 
-ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
+lemmas map_of_Cons = map_of.simps(2)
+
 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
 apply (simp (no_asm))
 done
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Jul 30 19:46:13 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Jul 30 19:46:15 2007 +0200
@@ -176,59 +176,61 @@
 contains
   test = "exec (E, start_state E test_name makelist_name)"
 
-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) *}
+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);
+*}
 
 end
isabelle