changeset 5253 | 82a5ca6290aa |
parent 5111 | 8f4b72f0c15d |
child 5277 | e4297d03e5d2 |
--- a/src/HOL/UNITY/SubstAx.thy Wed Aug 05 10:56:58 1998 +0200 +++ b/src/HOL/UNITY/SubstAx.thy Wed Aug 05 10:57:25 1998 +0200 @@ -10,10 +10,9 @@ constdefs - LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool" - "LeadsTo == %(Init,Acts) A B. - leadsTo Acts (reachable (Init,Acts) Int A) - (reachable (Init,Acts) Int B)" - - + LeadsTo :: "['a program, 'a set, 'a set] => bool" + "LeadsTo prg A B == + leadsTo (Acts prg) + (reachable prg Int A) + (reachable prg Int B)" end