src/HOL/Bali/AxSound.thy
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/Bali/AxSound.thy	Tue Jul 16 18:52:26 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Tue Jul 16 20:25:21 2002 +0200
     1.3 @@ -391,6 +391,9 @@
     1.4  
     1.5  (* BinOp *)
     1.6  apply (tactic "sound_forw_hyp_tac 1")
     1.7 +apply (case_tac "need_second_arg binop v1")
     1.8 +apply   fastsimp
     1.9 +apply   simp
    1.10  
    1.11  (* Ass *)
    1.12  apply (tactic "sound_forw_hyp_tac 1")