# HG changeset patch
# User wenzelm
# Date 1506965919 -7200
# Node ID 9312ce5a938df5217cd318f46a0f26951e86f133
# Parent  e32750d7acb42091326c063b2e0337edc4e1c59f
prefer file dependencies wrt. specific theories;

diff -r e32750d7acb4 -r 9312ce5a938d src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -192,6 +192,8 @@
 
 subsubsection \<open>Setting up the counterexample generator\<close>
 
+external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
+external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 ML_file "Tools/Quickcheck/narrowing_generators.ML"
 
 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
diff -r e32750d7acb4 -r 9312ce5a938d src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/ROOT	Mon Oct 02 19:38:39 2017 +0200
@@ -7,9 +7,6 @@
   theories
     Main (global)
     Complex_Main (global)
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   document_files
     "root.bib"
     "root.tex"
@@ -24,9 +21,6 @@
     "HOL-Library"
   theories
     "HOL-Library.Old_Datatype"
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
 session "HOL-Library" (main timing) in Library = HOL +
   description {*
@@ -848,12 +842,6 @@
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests
-  files
-    "Boogie_Dijkstra.certs"
-    "Boogie_Max.certs"
-    "SMT_Examples.certs"
-    "SMT_Word_Examples.certs"
-    "VCC_Max.certs"
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   options [document = false]
diff -r e32750d7acb4 -r 9312ce5a938d src/HOL/SMT_Examples/Boogie.thy
--- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -55,17 +55,20 @@
 declare [[smt_read_only_certificates = true]]
 
 
+external_file "Boogie_Max.certs"
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
 boogie_file Boogie_Max
 
 
+external_file "Boogie_Dijkstra.certs"
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
 boogie_file Boogie_Dijkstra
 
 
 declare [[z3_extensions = true]]
+external_file "VCC_Max.certs"
 declare [[smt_certificates = "VCC_Max.certs"]]
 
 boogie_file VCC_Max
diff -r e32750d7acb4 -r 9312ce5a938d src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:28:18 2017 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Oct 02 19:38:39 2017 +0200
@@ -8,6 +8,7 @@
 imports Complex_Main
 begin
 
+external_file "SMT_Examples.certs"
 declare [[smt_certificates = "SMT_Examples.certs"]]
 declare [[smt_read_only_certificates = true]]