src/HOL/Bali/Example.thy
changeset 26480 544cef16045b
parent 26342 0f65fa163304
child 28524 644b62cf678f
equal deleted inserted replaced
26479:3a2efce3e992 26480:544cef16045b
   892 done
   892 done
   893 
   893 
   894 
   894 
   895 declare member_is_static_simp [simp]
   895 declare member_is_static_simp [simp]
   896 declare wt.Skip [rule del] wt.Init [rule del]
   896 declare wt.Skip [rule del] wt.Init [rule del]
   897 ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
   897 ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *}
   898 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
   898 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
   899 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
   899 lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
   900 
   900 
   901 lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
   901 lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
   902 lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
   902 lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
  1190 declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
  1190 declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
  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 {* 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