src/HOL/HOL.ML
changeset 5154 40fd46f3d3a1
parent 5139 013ea0f023e3
child 5185 d1067e2c3f9f
     1.1 --- a/src/HOL/HOL.ML	Fri Jul 17 10:49:19 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Jul 17 10:50:01 1998 +0200
     1.3 @@ -335,7 +335,7 @@
     1.4  (* case distinction *)
     1.5  
     1.6  qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
     1.7 -  (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
     1.8 +  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
     1.9                    etac p2 1, etac p1 1]);
    1.10  
    1.11  fun case_tac a = res_inst_tac [("P",a)] case_split_thm;