src/HOL/Codatatype/Examples/Misc_Data.thy
changeset 49509 163914705f8d
parent 49463 83ac281bcdc2
     1.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Fri Sep 21 15:53:29 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Fri Sep 21 16:34:40 2012 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Codatatype/Examples/Misc_Data.thy
     1.5 +(*  Title:      HOL/BNF/Examples/Misc_Data.thy
     1.6      Author:     Dmitriy Traytel, TU Muenchen
     1.7      Author:     Andrei Popescu, TU Muenchen
     1.8      Copyright   2012
     1.9 @@ -9,7 +9,7 @@
    1.10  header {* Miscellaneous Datatype Declarations *}
    1.11  
    1.12  theory Misc_Data
    1.13 -imports "../Codatatype"
    1.14 +imports "../BNF"
    1.15  begin
    1.16  
    1.17  data simple = X1 | X2 | X3 | X4