prefer file dependencies wrt. specific theories;
authorwenzelm
Mon Oct 02 19:38:39 2017 +0200 (18 months ago)
changeset 667589312ce5a938d
parent 66757 e32750d7acb4
child 66759 918f15c9367a
prefer file dependencies wrt. specific theories;
src/HOL/Quickcheck_Narrowing.thy
src/HOL/ROOT
src/HOL/SMT_Examples/Boogie.thy
src/HOL/SMT_Examples/SMT_Examples.thy
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:28:18 2017 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:38:39 2017 +0200
     1.3 @@ -192,6 +192,8 @@
     1.4  
     1.5  subsubsection \<open>Setting up the counterexample generator\<close>
     1.6  
     1.7 +external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
     1.8 +external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     1.9  ML_file "Tools/Quickcheck/narrowing_generators.ML"
    1.10  
    1.11  definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
     2.1 --- a/src/HOL/ROOT	Mon Oct 02 19:28:18 2017 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Oct 02 19:38:39 2017 +0200
     2.3 @@ -7,9 +7,6 @@
     2.4    theories
     2.5      Main (global)
     2.6      Complex_Main (global)
     2.7 -  files
     2.8 -    "Tools/Quickcheck/Narrowing_Engine.hs"
     2.9 -    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    2.10    document_files
    2.11      "root.bib"
    2.12      "root.tex"
    2.13 @@ -24,9 +21,6 @@
    2.14      "HOL-Library"
    2.15    theories
    2.16      "HOL-Library.Old_Datatype"
    2.17 -  files
    2.18 -    "Tools/Quickcheck/Narrowing_Engine.hs"
    2.19 -    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    2.20  
    2.21  session "HOL-Library" (main timing) in Library = HOL +
    2.22    description {*
    2.23 @@ -848,12 +842,6 @@
    2.24      SMT_Examples
    2.25      SMT_Word_Examples
    2.26      SMT_Tests
    2.27 -  files
    2.28 -    "Boogie_Dijkstra.certs"
    2.29 -    "Boogie_Max.certs"
    2.30 -    "SMT_Examples.certs"
    2.31 -    "SMT_Word_Examples.certs"
    2.32 -    "VCC_Max.certs"
    2.33  
    2.34  session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
    2.35    options [document = false]
     3.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:28:18 2017 +0200
     3.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:38:39 2017 +0200
     3.3 @@ -55,17 +55,20 @@
     3.4  declare [[smt_read_only_certificates = true]]
     3.5  
     3.6  
     3.7 +external_file "Boogie_Max.certs"
     3.8  declare [[smt_certificates = "Boogie_Max.certs"]]
     3.9  
    3.10  boogie_file Boogie_Max
    3.11  
    3.12  
    3.13 +external_file "Boogie_Dijkstra.certs"
    3.14  declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    3.15  
    3.16  boogie_file Boogie_Dijkstra
    3.17  
    3.18  
    3.19  declare [[z3_extensions = true]]
    3.20 +external_file "VCC_Max.certs"
    3.21  declare [[smt_certificates = "VCC_Max.certs"]]
    3.22  
    3.23  boogie_file VCC_Max
     4.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:28:18 2017 +0200
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:38:39 2017 +0200
     4.3 @@ -8,6 +8,7 @@
     4.4  imports Complex_Main
     4.5  begin
     4.6  
     4.7 +external_file "SMT_Examples.certs"
     4.8  declare [[smt_certificates = "SMT_Examples.certs"]]
     4.9  declare [[smt_read_only_certificates = true]]
    4.10