equal
deleted
inserted
replaced
13 |
13 |
14 typedef (Program) |
14 typedef (Program) |
15 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}" |
15 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}" |
16 |
16 |
17 consts |
17 consts |
18 co, unless :: "['a set, 'a set] => 'a program set" (infixl 60) |
18 constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) |
|
19 op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) |
19 |
20 |
20 constdefs |
21 constdefs |
21 mk_program :: "('a set * ('a * 'a)set set) => 'a program" |
22 mk_program :: "('a set * ('a * 'a)set set) => 'a program" |
22 "mk_program == %(init, acts). Abs_Program (init, insert Id acts)" |
23 "mk_program == %(init, acts). Abs_Program (init, insert Id acts)" |
23 |
24 |