tuned dependencies
authorblanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12)
changeset 5724225aff3b8d550
parent 57241 7fca4159117f
child 57243 8c261f0a9b32
tuned dependencies
src/HOL/Nitpick.thy
src/HOL/Random.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/Nitpick.thy	Thu Jun 12 17:02:03 2014 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Thu Jun 12 17:02:03 2014 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     1.5  
     1.6  theory Nitpick
     1.7 -imports BNF_FP_Base Map Record
     1.8 +imports Record
     1.9  keywords
    1.10    "nitpick" :: diag and
    1.11    "nitpick_params" :: thy_decl
     2.1 --- a/src/HOL/Random.thy	Thu Jun 12 17:02:03 2014 +0200
     2.2 +++ b/src/HOL/Random.thy	Thu Jun 12 17:02:03 2014 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  header {* A HOL random engine *}
     2.5  
     2.6  theory Random
     2.7 -imports Code_Numeral List
     2.8 +imports List
     2.9  begin
    2.10  
    2.11  notation fcomp (infixl "\<circ>>" 60)
     3.1 --- a/src/HOL/Sledgehammer.thy	Thu Jun 12 17:02:03 2014 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Thu Jun 12 17:02:03 2014 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     3.5  
     3.6  theory Sledgehammer
     3.7 -imports Presburger ATP SMT2
     3.8 +imports Presburger SMT2
     3.9  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
    3.10  begin
    3.11