equal
deleted
inserted
replaced
14 |
14 |
15 extend_set :: "['a*'b => 'c, 'a set] => 'c set" |
15 extend_set :: "['a*'b => 'c, 'a set] => 'c set" |
16 "extend_set h A == h `` (A Times UNIV)" |
16 "extend_set h A == h `` (A Times UNIV)" |
17 |
17 |
18 extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set" |
18 extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set" |
19 "extend_act h == (%act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))})" |
19 "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}" |
20 |
20 |
21 extend :: "['a*'b => 'c, 'a program] => 'c program" |
21 extend :: "['a*'b => 'c, 'a program] => 'c program" |
22 "extend h F == mk_program (extend_set h (Init F), |
22 "extend h F == mk_program (extend_set h (Init F), |
23 extend_act h `` Acts F)" |
23 extend_act h `` Acts F)" |
24 |
24 |