--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue May 12 10:59:59 2020 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue May 12 15:52:17 2020 +0200
@@ -241,6 +241,7 @@
axiomatization
where ext [intro]: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
and iff [intro]: "(A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<longleftrightarrow> B"
+ for f g :: "'a \<Rightarrow> 'b"
lemma sym [sym]: "y = x" if "x = y"
using that by (rule subst) (rule refl)