src/HOL/MicroJava/J/JTypeSafe.thy
changeset 27215 b43785a81e01
parent 27118 9a26c0d7a47a
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jun 14 23:20:06 2008 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Jun 14 23:20:07 2008 +0200
     1.3 @@ -247,7 +247,7 @@
     1.4         THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
     1.5  
     1.6  -- "for if"
     1.7 -apply( tactic {* (case_split_tac "the_Bool v" THEN_ALL_NEW
     1.8 +apply( tactic {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
     1.9    (asm_full_simp_tac @{simpset})) 7*})
    1.10  
    1.11  apply (tactic "forward_hyp_tac")