src/FOL/FOL.thy

 ML {*
   fun excluded_middle_tac sP =
     res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
 *}
 
-lemma case_split_thm:
+lemma case_split [case_names True False]:
   assumes r1: "P ==> Q"
     and r2: "~P ==> Q"
   shows Q
   apply (rule excluded_middle [THEN disjE])
   apply (erule r2)
   apply (erule r1)
   done
 
-lemmas case_split = case_split_thm [case_names True False]
-
-(*HOL's more natural case analysis tactic*)
 ML {*
-  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
+  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split}
 *}
 
 
 (*** Special elimination rules *)