--- a/src/HOL/HOL.ML Fri Jul 17 10:49:19 1998 +0200
+++ b/src/HOL/HOL.ML Fri Jul 17 10:50:01 1998 +0200
@@ -335,7 +335,7 @@
(* case distinction *)
qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
- (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
+ (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
etac p2 1, etac p1 1]);
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
--- a/src/HOL/Update.ML Fri Jul 17 10:49:19 1998 +0200
+++ b/src/HOL/Update.ML Fri Jul 17 10:50:01 1998 +0200
@@ -18,6 +18,7 @@
(* f x = y ==> f(x:=y) = f *)
bind_thm("update_idem", update_idem_iff RS iffD2);
+(* f(x := f x) = f *)
AddIffs [refl RS update_idem];
Goal "(f(x:=y))z = (if z=x then y else f z)";