tuned imports
authorblanchet
Wed Sep 03 00:06:26 2014 +0200 (2014-09-03)
changeset 5815447c3c7019b97
parent 58153 ca7ea280e906
child 58155 14dda84afbb3
tuned imports
src/HOL/Main.thy
src/HOL/Num.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/Main.thy	Wed Sep 03 00:06:25 2014 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Sep 03 00:06:26 2014 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5  theory Main
     1.6  imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     1.7 -  BNF_Greatest_Fixpoint
     1.8 +  BNF_Greatest_Fixpoint Old_Datatype
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Num.thy	Wed Sep 03 00:06:25 2014 +0200
     2.2 +++ b/src/HOL/Num.thy	Wed Sep 03 00:06:26 2014 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Binary Numerals *}
     2.5  
     2.6  theory Num
     2.7 -imports BNF_Least_Fixpoint Old_Datatype
     2.8 +imports BNF_Least_Fixpoint
     2.9  begin
    2.10  
    2.11  subsection {* The @{text num} type *}
     3.1 --- a/src/HOL/Option.thy	Wed Sep 03 00:06:25 2014 +0200
     3.2 +++ b/src/HOL/Option.thy	Wed Sep 03 00:06:26 2014 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Datatype option *}
     3.5  
     3.6  theory Option
     3.7 -imports BNF_Least_Fixpoint Old_Datatype Finite_Set
     3.8 +imports BNF_Least_Fixpoint Finite_Set
     3.9  begin
    3.10  
    3.11  datatype_new 'a option =