# HG changeset patch
# User wenzelm
# Date 1007582280 -3600
# Node ID b20a37eb8338087334a251a51204a2edfdae4323
# Parent  03c55bb0ee926aa793c66dd3f6b4aedc037fb958
sym [sym];

diff -r 03c55bb0ee92 -r b20a37eb8338 src/HOL/ex/Higher_Order_Logic.thy
--- 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)