equal
deleted
inserted
replaced
6 S-expressions, general binary trees for defining recursive data structures |
6 S-expressions, general binary trees for defining recursive data structures |
7 *) |
7 *) |
8 |
8 |
9 Sexp = Univ + |
9 Sexp = Univ + |
10 consts |
10 consts |
11 sexp :: "'a item set" |
11 sexp :: 'a item set |
12 |
12 |
13 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
13 sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
14 'a item] => 'b" |
14 'a item] => 'b" |
15 |
15 |
16 sexp_rec :: "['a item, 'a=>'b, nat=>'b, |
16 sexp_rec :: "['a item, 'a=>'b, nat=>'b, |