--- a/src/HOL/ex/Argo_Examples.thy Mon Jul 31 15:38:21 2017 +0100
+++ b/src/HOL/ex/Argo_Examples.thy Tue Aug 01 07:26:23 2017 +0200
@@ -530,6 +530,9 @@
notepad
begin
+ fix a b :: real
+ have "f (a + b) = f (b + a)" by argo
+next
have
"(0::real) < 1"
"(47::real) + 11 < 8 * 15"