src/HOL/Bali/Example.thy
changeset 24019 67bde7cfcf10
parent 22708 fff918feff45
child 26342 0f65fa163304
     1.1 --- a/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -894,7 +894,7 @@
     1.4  
     1.5  declare member_is_static_simp [simp]
     1.6  declare wt.Skip [rule del] wt.Init [rule del]
     1.7 -ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
     1.8 +ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
     1.9  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    1.10  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    1.11  
    1.12 @@ -1192,10 +1192,10 @@
    1.13  declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
    1.14          Base_foo_defs  [simp]
    1.15  
    1.16 -ML {* bind_thms ("eval_intros", map 
    1.17 -        (simplify (simpset() delsimps [thm "Skip_eq"]
    1.18 -                             addsimps [thm "lvar_def"]) o 
    1.19 -         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
    1.20 +ML_setup {* bind_thms ("eval_intros", map 
    1.21 +        (simplify (simpset() delsimps @{thms Skip_eq}
    1.22 +                             addsimps @{thms lvar_def}) o 
    1.23 +         rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    1.24  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    1.25  
    1.26  consts