--- a/src/HOL/IMP/Abs_State.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/IMP/Abs_State.thy Tue Jan 16 09:30:00 2018 +0100
@@ -10,15 +10,15 @@
"fun_rep [] = (\<lambda>x. \<top>)" |
"fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
-lemma fun_rep_map_of[code]: \<comment>"original def is too slow"
+lemma fun_rep_map_of[code]: \<comment> \<open>original def is too slow\<close>
"fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
by(induction ps rule: fun_rep.induct) auto
definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
"eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
-hide_type st \<comment>"hide previous def to avoid long names"
-declare [[typedef_overloaded]] \<comment>"allow quotient types to depend on classes"
+hide_type st \<comment> \<open>hide previous def to avoid long names\<close>
+declare [[typedef_overloaded]] \<comment> \<open>allow quotient types to depend on classes\<close>
quotient_type 'a st = "('a::top) st_rep" / eq_st
morphisms rep_st St