| changeset 49076 | d2ed455fa3d2 |
| parent 48975 | 7f79f94a432c |
| child 49128 | 1a86ef0a0210 |
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Mon Sep 03 11:54:21 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Mon Sep 03 11:54:21 2012 +0200 @@ -15,7 +15,7 @@ typedecl N typedecl T -bnf_codata Tree: 'Tree = "N \<times> (T + 'Tree) fset" +codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset" section {* Sugar notations for Tree *}