tuned proofs -- case_tac *is* available here;
authorwenzelm
Tue Jun 10 19:15:18 2008 +0200 (2008-06-10)
changeset 271250733f575b51e
parent 27124 e02d6e655e60
child 27126 3ede9103de8e
tuned proofs -- case_tac *is* available here;
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Tue Jun 10 19:15:17 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue Jun 10 19:15:18 2008 +0200
     1.3 @@ -465,9 +465,8 @@
     1.4  
     1.5  lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
     1.6  apply (simp add: surj_def swap_def, clarify)
     1.7 -apply (rule_tac P = "y = f b" in case_split_thm, blast)
     1.8 -apply (rule_tac P = "y = f a" in case_split_thm, auto)
     1.9 -  --{*We don't yet have @{text case_tac}*}
    1.10 +apply (case_tac "y = f b", blast)
    1.11 +apply (case_tac "y = f a", auto)
    1.12  done
    1.13  
    1.14  lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"