tidying
authorpaulson
Fri Jul 17 10:50:01 1998 +0200 (1998-07-17)
changeset 515440fd46f3d3a1
parent 5153 51bd3cd9ee85
child 5155 21177b8a4d7f
tidying
src/HOL/HOL.ML
src/HOL/Update.ML
     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;
     2.1 --- a/src/HOL/Update.ML	Fri Jul 17 10:49:19 1998 +0200
     2.2 +++ b/src/HOL/Update.ML	Fri Jul 17 10:50:01 1998 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4  (* f x = y ==> f(x:=y) = f *)
     2.5  bind_thm("update_idem", update_idem_iff RS iffD2);
     2.6  
     2.7 +(* f(x := f x) = f *)
     2.8  AddIffs [refl RS update_idem];
     2.9  
    2.10  Goal "(f(x:=y))z = (if z=x then y else f z)";