| changeset 27118 | 9a26c0d7a47a |
| parent 27098 | d89fb4ee7280 |
| child 27215 | b43785a81e01 |
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Jun 10 16:43:14 2008 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Jun 10 16:43:16 2008 +0200 @@ -247,7 +247,7 @@ THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*}) -- "for if" -apply( tactic {* (DatatypePackage.case_tac "the_Bool v" THEN_ALL_NEW +apply( tactic {* (case_split_tac "the_Bool v" THEN_ALL_NEW (asm_full_simp_tac @{simpset})) 7*}) apply (tactic "forward_hyp_tac")