--- a/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:24:36 2015 +0100
+++ b/src/HOL/Proofs/Lambda/ListBeta.thy Wed Dec 30 18:25:39 2015 +0100
@@ -3,13 +3,13 @@
Copyright 1998 TU Muenchen
*)
-section {* Lifting beta-reduction to lists *}
+section \<open>Lifting beta-reduction to lists\<close>
theory ListBeta imports ListApplication ListOrder begin
-text {*
+text \<open>
Lifting beta-reduction to lists of terms, reducing exactly one element.
-*}
+\<close>
abbreviation
list_beta :: "dB list => dB list => bool" (infixl "=>" 50) where