tuned -- avoid warning;
authorwenzelm
Tue, 12 May 2020 15:52:17 +0200
changeset 72056 26c4af1e4ffe
parent 72053 7a997ead54b0
child 72057 f61b19358a8f
tuned -- avoid warning;
src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- 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)