# 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 \Setting up the counterexample generator\ +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]]