# HG changeset patch # User nipkow # Date 1515256481 -3600 # Node ID bf269672c203a78df602b4a4331759e3466d0d29 # Parent 1f1d85393d70513c3de64c37c1c12377538fea97 tuned op diff -r 1f1d85393d70 -r bf269672c203 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Jan 06 15:08:42 2018 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Jan 06 17:34:41 2018 +0100 @@ -759,7 +759,7 @@ text \Interpreted versions\ -lemma "0 = glob_one (op +)" by (rule int.def.one_def) +lemma "0 = glob_one ((op +))" by (rule int.def.one_def) lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def) text \Roundup applies rewrite morphisms at declaration level in DFS tree\