equal
deleted
inserted
replaced
14 hide_fact (open) Quotient_Product.prod_rel_def |
14 hide_fact (open) Quotient_Product.prod_rel_def |
15 |
15 |
16 typedecl N |
16 typedecl N |
17 typedecl T |
17 typedecl T |
18 |
18 |
19 codata dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
19 codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
20 |
20 |
21 subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} |
21 subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} |
22 |
22 |
23 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
23 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
24 definition "cont \<equiv> fset o ccont" |
24 definition "cont \<equiv> fset o ccont" |