# HG changeset patch
# User wenzelm
# Date 1589291537 -7200
# Node ID 26c4af1e4ffe0cc42a8cd5f29d9c4463f63de9a5
# Parent  7a997ead54b000a07d6b71012fe19cc7b187ae25
tuned -- avoid warning;

diff -r 7a997ead54b0 -r 26c4af1e4ffe 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)