# HG changeset patch
# User wenzelm
# Date 1213478403 -7200
# Node ID 3a3686dd4433c09cc76ab216ec7fc18ae401cdbe
# Parent  6724f31a1c8e06a51ebfe26eb6c5194bf915c349
removed obsolete case_split_tac -- cannot work without;

diff -r 6724f31a1c8e -r 3a3686dd4433 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jun 14 23:20:02 2008 +0200
+++ b/src/HOL/HOL.thy	Sat Jun 14 23:20:03 2008 +0200
@@ -731,10 +731,6 @@
 apply (erule prem1)
 done
 
-ML {*
-  fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
-*}
-
 (*Classical implies (-->) elimination. *)
 lemma impCE:
   assumes major: "P-->Q"