src/HOL/Bali/Example.thy
changeset 26342 0f65fa163304
parent 24019 67bde7cfcf10
child 26480 544cef16045b
equal deleted inserted replaced
26341:2f5a4367a39e 26342:0f65fa163304
  1191 declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
  1191 declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
  1192 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
  1192 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
  1193         Base_foo_defs  [simp]
  1193         Base_foo_defs  [simp]
  1194 
  1194 
  1195 ML_setup {* bind_thms ("eval_intros", map 
  1195 ML_setup {* bind_thms ("eval_intros", map 
  1196         (simplify (simpset() delsimps @{thms Skip_eq}
  1196         (simplify (@{simpset} delsimps @{thms Skip_eq}
  1197                              addsimps @{thms lvar_def}) o 
  1197                              addsimps @{thms lvar_def}) o 
  1198          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
  1198          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
  1199 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  1199 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  1200 
  1200 
  1201 consts
  1201 consts