src/HOL/Bali/AxSound.thy
changeset 13601 fd3e3d6b37b2
parent 13384 a34e38154413
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/AxSound.thy	Mon Sep 30 16:12:16 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Sep 30 16:14:02 2002 +0200
     1.3 @@ -102,8 +102,9 @@
     1.4  apply (drule triples_valid2_Suc)
     1.5  apply (erule (1) notE impE)
     1.6  apply (drule_tac x = na in spec)
     1.7 -apply (tactic {* auto_tac (claset() addSIs [thm "Methd_triple_valid2_SucI"],
     1.8 -   simpset() addsimps [ball_Un] addloop ("split_all_tac", split_all_tac)) *})
     1.9 +apply (rule Methd_triple_valid2_SucI)
    1.10 +apply (simp (no_asm_use) add: ball_Un)
    1.11 +apply auto
    1.12  done
    1.13  
    1.14  
    1.15 @@ -351,7 +352,7 @@
    1.16  apply (frule wf_ws_prog) 
    1.17  apply (frule ty_expr_is_type [THEN type_is_class, 
    1.18                                THEN accfield_declC_is_class])
    1.19 -apply (simp,simp,simp) 
    1.20 +apply (simp (no_asm_use), simp (no_asm_use), simp (no_asm_use))
    1.21  apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
    1.22  apply (tactic "ALLGOALS sound_valid2_tac")
    1.23  apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)