# HG changeset patch # User wenzelm # Date 1185817575 -7200 # Node ID 40f414b87655b7f0fb698a50d67addc730e7018d # Parent 373727835757dbdcc91839d2dd8fda4eb6400746 tuned ML declarations; diff -r 373727835757 -r 40f414b87655 src/HOL/MicroJava/Comp/CorrComp.thy --- 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: "\ wf_java_prog G; is_class G C; method (G, C) S = Some (D, rT, pns, lvars, blk, res) \ \ @@ -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] diff -r 373727835757 -r 40f414b87655 src/HOL/MicroJava/J/Example.thy --- 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\obj1),empty(x\Null)(This\Addr a))" abbreviation "s3 == (Some NP, empty(a\obj1),empty(e\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 diff -r 373727835757 -r 40f414b87655 src/HOL/MicroJava/JVM/JVMListExample.thy --- 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