| changeset 2642 | 3c3a84cc85a9 |
| parent 1479 | 21eb5e156d91 |
| child 10835 | f4745d77e620 |
| 2641:533a84b3bedd | 2642:3c3a84cc85a9 |
|---|---|
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Theory for a loop primitive like while |
6 Theory for a loop primitive like while |
7 *) |
7 *) |
8 |
8 |
9 Loop = Tr2 + |
9 Loop = Tr + |
10 |
10 |
11 consts |
11 consts |
12 |
|
13 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
12 step :: "('a -> tr)->('a -> 'a)->'a->'a" |
14 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
13 while :: "('a -> tr)->('a -> 'a)->'a->'a" |
15 |
14 |
16 defs |
15 defs |
17 |
16 |