changeset 5192 | 704dd3a6d47d |
parent 3522 | a34c20f4bf44 |
child 6468 | a7b1669f5365 |
5191:8ceaa19f7717 | 5192:704dd3a6d47d |
---|---|
26 rsch_fin_ioa :: ('m action, bool list)ioa |
26 rsch_fin_ioa :: ('m action, bool list)ioa |
27 |
27 |
28 reverse :: 'a list => 'a list |
28 reverse :: 'a list => 'a list |
29 |
29 |
30 primrec |
30 primrec |
31 reverse List.list |
|
32 reverse_Nil "reverse([]) = []" |
31 reverse_Nil "reverse([]) = []" |
33 reverse_Cons "reverse(x#xs) = reverse(xs)@[x]" |
32 reverse_Cons "reverse(x#xs) = reverse(xs)@[x]" |
34 |
33 |
35 defs |
34 defs |
36 |
35 |