--- a/src/HOL/MicroJava/DFA/Semilat.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,9 +3,9 @@
Copyright 2000 TUM
*)
-chapter {* Bytecode Verifier \label{cha:bv} *}
+chapter \<open>Bytecode Verifier \label{cha:bv}\<close>
-section {* Semilattices *}
+section \<open>Semilattices\<close>
theory Semilat
imports Main "~~/src/HOL/Library/While_Combinator"
@@ -301,7 +301,7 @@
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
(*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
-subsection{*An executable lub-finder*}
+subsection\<open>An executable lub-finder\<close>
definition exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" where
"exec_lub r f x y \<equiv> while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"