| changeset 27098 | d89fb4ee7280 |
| parent 24178 | 4ff1dc2aa18d |
| child 27118 | 9a26c0d7a47a |
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Jun 09 17:07:11 2008 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Jun 09 17:24:48 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 {* (case_tac "the_Bool v" THEN_ALL_NEW +apply( tactic {* (DatatypePackage.case_tac "the_Bool v" THEN_ALL_NEW (asm_full_simp_tac @{simpset})) 7*}) apply (tactic "forward_hyp_tac")