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/UNITY/ELT.thy
changeset 80914 d97fdabd9e2b
parent 67613 ce654b0e6d69 
--- a/src/HOL/UNITY/ELT.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/ELT.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -46,12 +46,12 @@
 definition
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
-                                        ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
+                                        (\<open>(3_/ leadsTo[_]/ _)\<close> [80,0,80] 80)
   where "leadsETo A CC B = {F. (A,B) \<in> elt CC F}"
 
 definition
   LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
-                                        ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
+                                        (\<open>(3_/ LeadsTo[_]/ _)\<close> [80,0,80] 80)
   where "LeadsETo A CC B =
       {F. F \<in> (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
isabelle