tuned proofs;
authorwenzelm
Tue Jun 10 16:43:16 2008 +0200 (2008-06-10)
changeset 271189a26c0d7a47a
parent 27117 97e9dae57284
child 27119 c36c88fcdd22
tuned proofs;
src/HOL/MicroJava/J/JTypeSafe.thy
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Jun 10 16:43:14 2008 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Jun 10 16:43:16 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 {* (DatatypePackage.case_tac "the_Bool v" THEN_ALL_NEW
     1.8 +apply( tactic {* (case_split_tac "the_Bool v" THEN_ALL_NEW
     1.9    (asm_full_simp_tac @{simpset})) 7*})
    1.10  
    1.11  apply (tactic "forward_hyp_tac")