Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned op
authornipkow
Sat, 06 Jan 2018 17:34:41 +0100
changeset 67347 bf269672c203
parent 67346 1f1d85393d70
child 67348 4c4db8687e50
tuned op
src/FOL/ex/Locale_Test/Locale_Test1.thy file | annotate | diff | comparison | revisions 
--- 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 \<open>Interpreted versions\<close>
 
-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 \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
isabelle