--- a/src/HOL/Data_Structures/Less_False.thy Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/Data_Structures/Less_False.thy Fri Jan 12 14:08:53 2018 +0100
@@ -1,12 +1,12 @@
(* Author: Tobias Nipkow *)
-section {* Improved Simproc for $<$ *}
+section \<open>Improved Simproc for $<$\<close>
theory Less_False
imports Main
begin
-simproc_setup less_False ("(x::'a::order) < y") = {* fn _ => fn ctxt => fn ct =>
+simproc_setup less_False ("(x::'a::order) < y") = \<open>fn _ => fn ctxt => fn ct =>
let
fun prp t thm = Thm.full_prop_of thm aconv t;
@@ -26,6 +26,6 @@
| SOME thm => NONE
end;
in prove_less_False (Thm.term_of ct) end
-*}
+\<close>
end