| changeset 60500 | 903bb1495239 | 
| parent 58881 | b9556a055632 | 
| child 60679 | ade12ef2773c | 
--- a/src/HOL/Library/Prefix_Order.thy Wed Jun 17 10:57:11 2015 +0200 +++ b/src/HOL/Library/Prefix_Order.thy Wed Jun 17 11:03:05 2015 +0200 @@ -2,7 +2,7 @@ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen *) -section {* Prefix order on lists as order class instance *} +section \<open>Prefix order on lists as order class instance\<close> theory Prefix_Order imports Sublist