removed obsolete case_split_tac -- cannot work without;
authorwenzelm
Sat Jun 14 23:20:03 2008 +0200 (2008-06-14)
changeset 272123a3686dd4433
parent 27211 6724f31a1c8e
child 27213 2c7a628ccdcf
removed obsolete case_split_tac -- cannot work without;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Jun 14 23:20:02 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jun 14 23:20:03 2008 +0200
     1.3 @@ -731,10 +731,6 @@
     1.4  apply (erule prem1)
     1.5  done
     1.6  
     1.7 -ML {*
     1.8 -  fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
     1.9 -*}
    1.10 -
    1.11  (*Classical implies (-->) elimination. *)
    1.12  lemma impCE:
    1.13    assumes major: "P-->Q"