# HG changeset patch
# User paulson
# Date 900665401 -7200
# Node ID 40fd46f3d3a16978f691d64633dd61cf120fae0e
# Parent  51bd3cd9ee85f7ed4675f5d5b6e20574b5ae6587
tidying

diff -r 51bd3cd9ee85 -r 40fd46f3d3a1 src/HOL/HOL.ML
--- 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;
diff -r 51bd3cd9ee85 -r 40fd46f3d3a1 src/HOL/Update.ML
--- 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)";