# HG changeset patch
# User wenzelm
# Date 1515359939 -3600
# Node ID 86aa6e2abee15f911ec164bce5f405cf26e9c86c
# Parent  63d7aca15f6b1ae41f91bee3f9f75036dbfc0273# Parent  7360fe6bb423acd25202e38745d10aaa47e48db1
merged

diff -r 7360fe6bb423 -r 86aa6e2abee1 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 07 22:15:54 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 07 22:18:59 2018 +0100
@@ -1555,8 +1555,8 @@
   quantifiers are transferred.
 
   \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
-  relators of various type constructors, e.g. @{term "rel_set (op =) = (op
-  =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
+  relators of various type constructors, e.g. @{term "rel_set (op =) = (op =)"}.
+  The @{method (HOL) transfer} method uses these lemmas to infer
   transfer rules for non-polymorphic constants on the fly. For examples see
   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
   is proved automatically if the involved type is BNF without dead variables.
diff -r 7360fe6bb423 -r 86aa6e2abee1 src/Doc/Locales/Examples2.thy
--- a/src/Doc/Locales/Examples2.thy	Sun Jan 07 22:15:54 2018 +0100
+++ b/src/Doc/Locales/Examples2.thy	Sun Jan 07 22:18:59 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
 
diff -r 7360fe6bb423 -r 86aa6e2abee1 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sun Jan 07 22:15:54 2018 +0100
+++ b/src/Doc/System/Presentation.thy	Sun Jan 07 22:18:59 2018 +0100
@@ -167,7 +167,7 @@
   run.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
+  Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
   is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
   will appear in the parent of this directory.
 
diff -r 7360fe6bb423 -r 86aa6e2abee1 src/Doc/Tutorial/Misc/simp.thy
--- a/src/Doc/Tutorial/Misc/simp.thy	Sun Jan 07 22:15:54 2018 +0100
+++ b/src/Doc/Tutorial/Misc/simp.thy	Sun Jan 07 22:18:59 2018 +0100
@@ -388,7 +388,7 @@
 [1]Rewriting:
 rev [] \(\equiv\) []
 
-[1]Applying instance of rewrite rule "List.op @.append_Nil":
+[1]Applying instance of rewrite rule "List.append.append_Nil":
 [] @ ?y \(\equiv\) ?y
 
 [1]Rewriting:
diff -r 7360fe6bb423 -r 86aa6e2abee1 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sun Jan 07 22:15:54 2018 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sun Jan 07 22:18:59 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>