| changeset 53013 | 3fbcfa911863 |
| parent 51804 | be6e703908f4 |
| child 54014 | 21dac9a60f0c |
--- a/src/HOL/BNF/Examples/TreeFsetI.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy Tue Aug 13 15:59:22 2013 +0200 @@ -12,7 +12,7 @@ imports "../BNF" begin -hide_fact (open) Quotient_Product.prod_rel_def +hide_fact (open) Lifting_Product.prod_rel_def codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")