--- 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.
--- 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
--- 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.
--- 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:
--- 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>