--- a/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 10:53:24 2014 +0200
+++ b/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 10:58:19 2014 +0200
@@ -2,7 +2,7 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Bounds *}
+header \<open>Bounds\<close>
theory Bounds
imports Main "~~/src/HOL/Library/ContNotDenum"
@@ -28,7 +28,7 @@
interpret lub A x by fact
show ?thesis
proof (unfold the_lub_def)
- from `lub A x` show "The (lub A) = x"
+ from \<open>lub A x\<close> show "The (lub A) = x"
proof
fix x' assume lub': "lub A x'"
show "x' = x"