xsymbols for leads-to and Join
authorpaulson
Thu Aug 24 12:39:24 2000 +0200 (2000-08-24)
changeset 96856d123a7e30bd
parent 9684 6b7d7635a062
child 9686 87b460d72e80
xsymbols for leads-to and Join
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 11:14:21 2000 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 12:39:24 2000 +0200
     1.3 @@ -15,4 +15,7 @@
     1.4     LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
     1.5      "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
     1.9 +
    1.10  end
     2.1 --- a/src/HOL/UNITY/Union.thy	Thu Aug 24 11:14:21 2000 +0200
     2.2 +++ b/src/HOL/UNITY/Union.thy	Thu Aug 24 12:39:24 2000 +0200
     2.3 @@ -29,4 +29,10 @@
     2.4    "JN x y. B"   == "JN x. JN y. B"
     2.5    "JN x. B"     == "JOIN UNIV (%x. B)"
     2.6  
     2.7 +syntax (symbols)
     2.8 +  SKIP      :: 'a program                              ("\\<bottom>")
     2.9 +  "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
    2.10 +  "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)
    2.11 +  "@JOIN"   :: [pttrn, 'a set, 'b set] => 'b set       ("(3\\<Squnion> _:_./ _)" 10)
    2.12 +
    2.13  end
     3.1 --- a/src/HOL/UNITY/WFair.thy	Thu Aug 24 11:14:21 2000 +0200
     3.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Aug 24 12:39:24 2000 +0200
     3.3 @@ -52,4 +52,7 @@
     3.4    wlt :: "['a program, 'a set] => 'a set"
     3.5      "wlt F B == Union {A. F: A leadsTo B}"
     3.6  
     3.7 +syntax (xsymbols)
     3.8 +  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
     3.9 +
    3.10  end