equal
deleted
inserted
replaced
20 (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)" |
20 (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)" |
21 *) |
21 *) |
22 |
22 |
23 header {*Definition of type llist by a greatest fixed point*} |
23 header {*Definition of type llist by a greatest fixed point*} |
24 |
24 |
25 theory LList imports Main SList begin |
25 theory LList imports SList begin |
26 |
26 |
27 consts |
27 consts |
28 |
28 |
29 llist :: "'a item set => 'a item set" |
29 llist :: "'a item set => 'a item set" |
30 LListD :: "('a item * 'a item)set => ('a item * 'a item)set" |
30 LListD :: "('a item * 'a item)set => ('a item * 'a item)set" |