[isabelle-dev] AFP dependencies: Refine_Imperative_HOL

[Makarius]

Here is some further simplification proposed by "isabelle imports -I".

One could probably also eliminate Sepref_Prereq. The maintainers of
these AFP entries need to say what is the purpose of that extra complexity.

(In the months before the Isabelle2017 release, I spent considerable
time to disentangle Sepref_Prereq, Refine_Imperative_HOL, Sepref_Basic,
Sepref_IICF -- and only now it becomes clear that there is not much
behind it.)


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1507844154 -7200
#      Thu Oct 12 23:35:54 2017 +0200
# Node ID 3f1af47f00bb8be309f6b749f24650145dffc4b4
# Parent  ddf5e04d1e6dec093eb9c8883abd916b49463c94
simplified session structure: full Refine_Imperative_HOL is already quite small (4min elapsed time, 12min CPU time, 4 threads);

diff -r ddf5e04d1e6d -r 3f1af47f00bb thys/Flow_Networks/ROOT
--- a/thys/Flow_Networks/ROOT	Thu Oct 12 22:45:03 2017 +0200
+++ b/thys/Flow_Networks/ROOT	Thu Oct 12 23:35:54 2017 +0200
@@ -1,6 +1,6 @@
 chapter AFP
 
-session Maxflow_Lib (AFP) = Sepref_IICF +
+session Maxflow_Lib (AFP) = Refine_Imperative_HOL +
   options [document = false, timeout = 600]
   sessions
     "Program-Conflict-Analysis"
diff -r ddf5e04d1e6d -r 3f1af47f00bb thys/Refine_Imperative_HOL/ROOT
--- a/thys/Refine_Imperative_HOL/ROOT	Thu Oct 12 22:45:03 2017 +0200
+++ b/thys/Refine_Imperative_HOL/ROOT	Thu Oct 12 23:35:54 2017 +0200
@@ -66,21 +66,3 @@
 
   document_files
     "root.tex"
-
-
-(* Smaller Sessions: *)
-session Sepref_Basic (AFP) = Sepref_Prereq +
-  options [document = false, timeout = 300]
-  sessions
-    "HOL-Eisbach"
-    "List-Index"
-    Refine_Imperative_HOL
-  theories [document = false]
-    Refine_Imperative_HOL.Sepref
-
-session Sepref_IICF (AFP) = Sepref_Basic +
-  options [document = false, timeout = 600]
-  sessions
-    Refine_Imperative_HOL
-  theories [document = false]
-    Refine_Imperative_HOL.IICF