src/HOL/Sum.ML
changeset 1264 3eb91524b938
parent 1188 0443e4dc8511
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Sum.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/Sum.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -44,11 +44,11 @@
     1.4  val Inr_neq_Inl = sym RS Inl_neq_Inr;
     1.5  
     1.6  goal Sum.thy "(Inl(a)=Inr(b)) = False";
     1.7 -by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
     1.8 +by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
     1.9  qed "Inl_Inr_eq";
    1.10  
    1.11  goal Sum.thy "(Inr(b)=Inl(a))  =  False";
    1.12 -by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
    1.13 +by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
    1.14  qed "Inr_Inl_eq";
    1.15  
    1.16  
    1.17 @@ -157,8 +157,7 @@
    1.18  by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    1.19  qed "expand_sum_case";
    1.20  
    1.21 -val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, 
    1.22 -			       sum_case_Inl, sum_case_Inr];
    1.23 +Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
    1.24  
    1.25  (*Prevents simplification of f and g: much faster*)
    1.26  qed_goal "sum_case_weak_cong" Sum.thy