Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proofs;
authorwenzelm
Tue, 10 Jun 2008 16:43:16 +0200
changeset 27118 9a26c0d7a47a
parent 27117 97e9dae57284
child 27119 c36c88fcdd22
tuned proofs;
src/HOL/MicroJava/J/JTypeSafe.thy file | annotate | diff | comparison | revisions 
--- 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")
isabelle