| changeset 12394 | b20a37eb8338 |
| parent 12360 | 9c156045c8f2 |
| child 12573 | 6226b35c04ca |
--- 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)