| changeset 9685 | 6d123a7e30bd |
| parent 8006 | 299127ded09d |
| child 10293 | 354e885b3e0a |
--- 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