src/HOL/UNITY/WFair.thy
changeset 9685 6d123a7e30bd
parent 8006 299127ded09d
child 10293 354e885b3e0a
equal deleted inserted replaced
9684:6b7d7635a062 9685:6d123a7e30bd
    50   
    50   
    51   (*wlt F B is the largest set that leads to B*)
    51   (*wlt F B is the largest set that leads to B*)
    52   wlt :: "['a program, 'a set] => 'a set"
    52   wlt :: "['a program, 'a set] => 'a set"
    53     "wlt F B == Union {A. F: A leadsTo B}"
    53     "wlt F B == Union {A. F: A leadsTo B}"
    54 
    54 
       
    55 syntax (xsymbols)
       
    56   "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
       
    57 
    55 end
    58 end