Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/ex/Locale_Test/Locale_Test1.thy
changeset 43543 eb8b4851b039
parent 41779 a68f503805ed
child 49756 28e37eab4e6f 
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Jun 23 23:12:00 2011 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Jun 25 12:19:54 2011 +0200
@@ -499,7 +499,7 @@
 end
 
 interpretation x: logic_o "op &" "Not"
-  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+  where bool_logic_o: "x.lor_o(x, y) <-> x | y"
 proof -
   show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
   show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
isabelle