moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
authorblanchet
Wed Oct 31 11:23:21 2012 +0100 (2012-10-31)
changeset 4998934d0ac1bdac6
parent 49988 ef811090e106
child 49990 42209bfa1548
moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
src/HOL/FunDef.thy
src/HOL/Nitpick.thy
src/HOL/SAT.thy
     1.1 --- a/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
     1.3 @@ -5,13 +5,10 @@
     1.4  header {* Function Definitions and Termination Proofs *}
     1.5  
     1.6  theory FunDef
     1.7 -imports Partial_Function Wellfounded
     1.8 +imports Partial_Function SAT Wellfounded
     1.9  keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
    1.10  begin
    1.11  
    1.12 -ML_file "Tools/prop_logic.ML"
    1.13 -ML_file "Tools/sat_solver.ML"
    1.14 -
    1.15  subsection {* Definitions with default value. *}
    1.16  
    1.17  definition
     2.1 --- a/src/HOL/Nitpick.thy	Wed Oct 31 11:23:21 2012 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Wed Oct 31 11:23:21 2012 +0100
     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 Map Quotient SAT Record
     2.8 +imports Hilbert_Choice List Map Quotient Record Sledgehammer
     2.9  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
     3.2 +++ b/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
     3.3 @@ -2,15 +2,17 @@
     3.4      Author:     Alwen Tiu, Tjark Weber
     3.5      Copyright   2005
     3.6  
     3.7 -Basic setup for the 'sat' and 'satx' tactic.
     3.8 +Basic setup for the 'sat' and 'satx' tactics.
     3.9  *)
    3.10  
    3.11  header {* Reconstructing external resolution proofs for propositional logic *}
    3.12  
    3.13  theory SAT
    3.14 -imports Hilbert_Choice List Sledgehammer
    3.15 +imports HOL
    3.16  begin
    3.17  
    3.18 +ML_file "Tools/prop_logic.ML"
    3.19 +ML_file "Tools/sat_solver.ML"
    3.20  ML_file "Tools/sat_funcs.ML"
    3.21  
    3.22  ML {* structure sat = SATFunc(cnf) *}