equal
deleted
inserted
replaced
8 header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} |
8 header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} |
9 |
9 |
10 theory DTree |
10 theory DTree |
11 imports Prelim |
11 imports Prelim |
12 begin |
12 begin |
13 |
|
14 hide_fact (open) Lifting_Product.prod_rel_def |
|
15 |
13 |
16 typedecl N |
14 typedecl N |
17 typedecl T |
15 typedecl T |
18 |
16 |
19 codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
17 codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") |