# 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>\~~/src/HOL/Lifting_Set.thy\ or \<^file>\~~/src/HOL/Lifting.thy\. 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 \\normalsize The second goal is shown by unfolding the definition of @{term "partial_order.less"}.\ show "partial_order.less op \ x y = (x < y)" - unfolding partial_order.less_def [OF \partial_order op \\] + unfolding partial_order.less_def [OF \partial_order (op \)\] 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>\-d\ specifies an laternative document output directory. The default + Option \<^verbatim>\-d\ specifies an alternative document output directory. The default is \<^verbatim>\output/document\ (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 \Interpreted versions\ -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 \Roundup applies rewrite morphisms at declaration level in DFS tree\