src/HOL/Relation.ML
changeset 1264 3eb91524b938
parent 1128 64b30e3cc6d4
child 1454 d0266c81a85e
     1.1 --- a/src/HOL/Relation.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/Relation.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  (** Natural deduction for converse(r) **)
     1.5  
     1.6  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
     1.7 -by (simp_tac prod_ss 1);
     1.8 +by (Simp_tac 1);
     1.9  by (fast_tac set_cs 1);
    1.10  qed "converseI";
    1.11  
    1.12 @@ -170,4 +170,4 @@
    1.13  
    1.14  val rel_eq_cs = rel_cs addSIs [equalityI];
    1.15  
    1.16 -val rel_ss = prod_ss addsimps [pair_in_id_conv];
    1.17 +Addsimps [pair_in_id_conv];