| changeset 50533 | fdda3c18dbcd |
| parent 49606 | afc7f88370a8 |
| child 51766 | f19a4d0ab1bf |
--- a/src/HOL/BNF/Examples/TreeFI.thy Thu Dec 13 09:21:45 2012 +0100 +++ b/src/HOL/BNF/Examples/TreeFI.thy Thu Dec 13 12:48:45 2012 +0100 @@ -12,8 +12,6 @@ imports ListF begin -hide_const (open) Sublist.sub - codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF") lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"