reduces Sledgehammer dependencies
authorblanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 57231dca8d06ecbba
parent 57230 ec5ff6bb2a92
child 57232 8cecd655eef4
reduces Sledgehammer dependencies
src/HOL/List.thy
src/HOL/Nitpick.thy
src/HOL/SMT.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/List.thy	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The datatype of finite lists *}
     1.5  
     1.6  theory List
     1.7 -imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     1.8 +imports Sledgehammer Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     1.9  begin
    1.10  
    1.11  datatype_new (set: 'a) list =
     2.1 --- a/src/HOL/Nitpick.thy	Thu Jun 12 01:00:49 2014 +0200
     2.2 +++ b/src/HOL/Nitpick.thy	Thu Jun 12 01:00:49 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     2.5  
     2.6  theory Nitpick
     2.7 -imports BNF_FP_Base Map Record Sledgehammer
     2.8 +imports BNF_FP_Base Map Record
     2.9  keywords
    2.10    "nitpick" :: diag and
    2.11    "nitpick_params" :: thy_decl
     3.1 --- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     3.2 +++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     3.5  
     3.6  theory SMT
     3.7 -imports ATP
     3.8 +imports Record
     3.9  keywords "smt_status" :: diag
    3.10  begin
    3.11  
     4.1 --- a/src/HOL/Sledgehammer.thy	Thu Jun 12 01:00:49 2014 +0200
     4.2 +++ b/src/HOL/Sledgehammer.thy	Thu Jun 12 01:00:49 2014 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     4.5  
     4.6  theory Sledgehammer
     4.7 -imports ATP SMT2
     4.8 +imports Presburger ATP SMT2
     4.9  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
    4.10  begin
    4.11