src/HOL/ex/Higher_Order_Logic.thy
changeset 12394 b20a37eb8338
parent 12360 9c156045c8f2
child 12573 6226b35c04ca
     1.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Dec 05 15:45:24 2001 +0100
     1.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Dec 05 20:58:00 2001 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
     1.5    iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A = B"
     1.6  
     1.7 -theorem sym [elim]: "x = y \<Longrightarrow> y = x"
     1.8 +theorem sym [sym]: "x = y \<Longrightarrow> y = x"
     1.9  proof -
    1.10    assume "x = y"
    1.11    thus "y = x" by (rule subst) (rule refl)