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:41:21 +0100
changeset 67349 0441f2f1b574
parent 67348 4c4db8687e50
child 67350 f061129d891b
tuned op
src/Doc/Locales/Examples2.thy file | annotate | diff | comparison | revisions 
--- a/src/Doc/Locales/Examples2.thy	Sat Jan 06 17:39:32 2018 +0100
+++ b/src/Doc/Locales/Examples2.thy	Sat Jan 06 17:41:21 2018 +0100
@@ -12,7 +12,7 @@
     txt \<open>\normalsize The second goal is shown by unfolding the
       definition of @{term "partial_order.less"}.\<close>
     show "partial_order.less op \<le> x y = (x < y)"
-      unfolding partial_order.less_def [OF \<open>partial_order op \<le>\<close>]
+      unfolding partial_order.less_def [OF \<open>partial_order (op \<le>)\<close>]
       by auto
   qed
isabelle