sym [sym];

--- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Dec 05 15:45:24 2001 +0100
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Dec 05 20:58:00 2001 +0100
@@ -56,7 +56,7 @@
   ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
 
-theorem sym [elim]: "x = y \<Longrightarrow> y = x"
+theorem sym [sym]: "x = y \<Longrightarrow> y = x"
 proof -
   assume "x = y"
   thus "y = x" by (rule subst) (rule refl)