Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Abs_Int2_ivl.thy
changeset 80914 d97fdabd9e2b
parent 77136 5bf9a1b78f93 
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -21,7 +21,7 @@
 quotient_type ivl = eint2 / eq_ivl
 by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
 
-abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_, _]") where
+abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" (\<open>[_, _]\<close>) where
 "[l,h] == abs_ivl(l,h)"
 
 lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
isabelle