# HG changeset patch
# User wenzelm
# Date 1213118118 -7200
# Node ID 0733f575b51e9c6c1ec30766fd03a6ea4cf7c73c
# Parent  e02d6e655e601342d184c74a1c19857196d80c0b
tuned proofs -- case_tac *is* available here;

diff -r e02d6e655e60 -r 0733f575b51e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jun 10 19:15:17 2008 +0200
+++ b/src/HOL/Fun.thy	Tue Jun 10 19:15:18 2008 +0200
@@ -465,9 +465,8 @@
 
 lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
 apply (simp add: surj_def swap_def, clarify)
-apply (rule_tac P = "y = f b" in case_split_thm, blast)
-apply (rule_tac P = "y = f a" in case_split_thm, auto)
-  --{*We don't yet have @{text case_tac}*}
+apply (case_tac "y = f b", blast)
+apply (case_tac "y = f a", auto)
 done
 
 lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"