src/HOL/UNITY/Union.thy
changeset 12114 a8e860c86252
parent 10064 1a77667b21ef
child 13792 d1811693899c
     1.1 --- a/src/HOL/UNITY/Union.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    "JN x y. B"   == "JN x. JN y. B"
     1.5    "JN x. B"     == "JOIN UNIV (%x. B)"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    SKIP      :: 'a program                              ("\\<bottom>")
    1.10    "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
    1.11    "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)