src/HOL/MicroJava/J/JTypeSafe.thy
changeset 45133 2214ba5bdfff
parent 41589 bbd861837ebc
child 51304 0e71a248cacb
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:21:38 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:48:23 2011 +0200
     1.3 @@ -243,7 +243,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 {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
     1.8 +apply( tactic {* (Induct_Tacs.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")