equal
deleted
inserted
replaced
16 tree have distinct names. This setup leads to logarithmic certificates. |
16 tree have distinct names. This setup leads to logarithmic certificates. |
17 *} |
17 *} |
18 |
18 |
19 subsection {* The Binary Tree *} |
19 subsection {* The Binary Tree *} |
20 |
20 |
21 datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip |
21 datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip |
22 |
22 |
23 |
23 |
24 text {* The boolean flag in the node marks the content of the node as |
24 text {* The boolean flag in the node marks the content of the node as |
25 deleted, without having to build a new tree. We prefer the boolean |
25 deleted, without having to build a new tree. We prefer the boolean |
26 flag to an option type, so that the ML-layer can still use the node |
26 flag to an option type, so that the ML-layer can still use the node |