'symmetric' attribute;

--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Aug 17 10:33:37 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Aug 17 10:34:11 2000 +0200
@@ -290,7 +290,7 @@
       by (rule tiling_domino_01);
     also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
     also; from t''; have "card ... = card (?e ?t'' 0)";
-      by (rule tiling_domino_01 [RS sym]);
+      by (rule tiling_domino_01 [symmetric]);
     finally; have "... < ..."; .; thus False; ..;
   qed;
 qed;

--- a/src/HOL/Isar_examples/W_correct.thy	Thu Aug 17 10:33:37 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Aug 17 10:34:11 2000 +0200
@@ -126,7 +126,7 @@
           by (simp add: subst_comp_tel o_def);
         show "$s a |- e1 :: $ u t2 -> t";
         proof -;
-          from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
+          from hyp1 W1_ok [symmetric]; have "$ s1 a |- e1 :: t1";
             by blast;
           hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
             by (intro has_type_subst_closed);
@@ -134,7 +134,7 @@
         qed;
         show "$ s a |- e2 :: $ u t2";
         proof -;
-          from hyp2 W2_ok [RS sym];
+          from hyp2 W2_ok [symmetric];
           have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
           hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
             by (rule has_type_subst_closed);
@@ -143,7 +143,7 @@
       qed;
     };
   qed;
-  with W_ok [RS sym]; show ?thesis; by blast;
+  with W_ok [symmetric]; show ?thesis; by blast;
 qed;
 
 end;