# HG changeset patch # User wenzelm # Date 1267614179 -3600 # Node ID a4babce15c67f7e4669f6c3202148efa7d225b61 # Parent 73cc288b4f83ae3492ce04968689545d5333e4c4 notation for xsymbols (cf. ad039d29e01c); diff -r 73cc288b4f83 -r a4babce15c67 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Mar 03 00:50:47 2010 +0100 +++ b/src/HOL/UNITY/Union.thy Wed Mar 03 12:02:59 2010 +0100 @@ -35,7 +35,7 @@ safety_prop :: "'a program set => bool" "safety_prop X == SKIP: X & (\G. Acts G \ UNION X Acts --> G \ X)" -notation +notation (xsymbols) SKIP ("\") and Join (infixl "\" 65)