# HG changeset patch
# User paulson
# Date 967113564 -7200
# Node ID 6d123a7e30bd15982b938cccc6099955935f3f28
# Parent  6b7d7635a0629c32dff590524915c8f90a51a706
xsymbols for leads-to and Join

diff -r 6b7d7635a062 -r 6d123a7e30bd src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 11:14:21 2000 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 12:39:24 2000 +0200
@@ -15,4 +15,7 @@
    LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
     "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
 
+syntax (xsymbols)
+  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
+
 end
diff -r 6b7d7635a062 -r 6d123a7e30bd src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Aug 24 11:14:21 2000 +0200
+++ b/src/HOL/UNITY/Union.thy	Thu Aug 24 12:39:24 2000 +0200
@@ -29,4 +29,10 @@
   "JN x y. B"   == "JN x. JN y. B"
   "JN x. B"     == "JOIN UNIV (%x. B)"
 
+syntax (symbols)
+  SKIP      :: 'a program                              ("\\<bottom>")
+  "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
+  "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)
+  "@JOIN"   :: [pttrn, 'a set, 'b set] => 'b set       ("(3\\<Squnion> _:_./ _)" 10)
+
 end
diff -r 6b7d7635a062 -r 6d123a7e30bd src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Thu Aug 24 11:14:21 2000 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Aug 24 12:39:24 2000 +0200
@@ -52,4 +52,7 @@
   wlt :: "['a program, 'a set] => 'a set"
     "wlt F B == Union {A. F: A leadsTo B}"
 
+syntax (xsymbols)
+  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
+
 end