changeset 26342 | 0f65fa163304 |
parent 24019 | 67bde7cfcf10 |
child 26480 | 544cef16045b |
--- a/src/HOL/Bali/Example.thy Wed Mar 19 22:47:39 2008 +0100 +++ b/src/HOL/Bali/Example.thy Wed Mar 19 22:50:42 2008 +0100 @@ -1193,7 +1193,7 @@ Base_foo_defs [simp] ML_setup {* bind_thms ("eval_intros", map - (simplify (simpset() delsimps @{thms Skip_eq} + (simplify (@{simpset} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *} lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros