# HG changeset patch
# User wenzelm
# Date 1636398904 -3600
# Node ID 0580ae467ecbb1eae7a04bc6c261904c7406f4a9
# Parent  f345da8defff747aeda6bb556acd0c223d908e27
tuned;

diff -r f345da8defff -r 0580ae467ecb src/HOL/ex/Argo_Examples.thy
--- 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