--- a/src/HOL/ex/Argo_Examples.thy Mon Nov 08 19:25:17 2021 +0100
+++ b/src/HOL/ex/Argo_Examples.thy Mon Nov 08 20:15:04 2021 +0100
@@ -531,6 +531,7 @@
notepad
begin
fix a b :: real
+ fix f :: "real \<Rightarrow> 'a"
have "f (a + b) = f (b + a)" by argo
next
have