# HG changeset patch
# User wenzelm
# Date 1506960688 -7200
# Node ID 1ceedf7105649f2b0a1af61b2e2e64fd0e7bad87
# Parent  78c74f9e960a1fa6d049d9e9045df7ea7fcf54f7
removed pointless dependencies: done by 'spark_open';

diff -r 78c74f9e960a -r 1ceedf710564 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Oct 02 16:47:46 2017 +0200
+++ b/src/HOL/ROOT	Mon Oct 02 18:11:28 2017 +0200
@@ -865,9 +865,7 @@
   options [document = false, spark_prv = false]
   theories
     "Gcd/Greatest_Common_Divisor"
-
     "Liseq/Longest_Increasing_Subsequence"
-
     "RIPEMD-160/F"
     "RIPEMD-160/Hash"
     "RIPEMD-160/K_L"
@@ -877,42 +875,7 @@
     "RIPEMD-160/R_R"
     "RIPEMD-160/S_L"
     "RIPEMD-160/S_R"
-
     "Sqrt/Sqrt"
-  files
-    "Gcd/greatest_common_divisor/g_c_d.fdl"
-    "Gcd/greatest_common_divisor/g_c_d.rls"
-    "Gcd/greatest_common_divisor/g_c_d.siv"
-    "Liseq/liseq/liseq_length.fdl"
-    "Liseq/liseq/liseq_length.rls"
-    "Liseq/liseq/liseq_length.siv"
-    "RIPEMD-160/rmd/f.fdl"
-    "RIPEMD-160/rmd/f.rls"
-    "RIPEMD-160/rmd/f.siv"
-    "RIPEMD-160/rmd/hash.fdl"
-    "RIPEMD-160/rmd/hash.rls"
-    "RIPEMD-160/rmd/hash.siv"
-    "RIPEMD-160/rmd/k_l.fdl"
-    "RIPEMD-160/rmd/k_l.rls"
-    "RIPEMD-160/rmd/k_l.siv"
-    "RIPEMD-160/rmd/k_r.fdl"
-    "RIPEMD-160/rmd/k_r.rls"
-    "RIPEMD-160/rmd/k_r.siv"
-    "RIPEMD-160/rmd/r_l.fdl"
-    "RIPEMD-160/rmd/r_l.rls"
-    "RIPEMD-160/rmd/r_l.siv"
-    "RIPEMD-160/rmd/round.fdl"
-    "RIPEMD-160/rmd/round.rls"
-    "RIPEMD-160/rmd/round.siv"
-    "RIPEMD-160/rmd/r_r.fdl"
-    "RIPEMD-160/rmd/r_r.rls"
-    "RIPEMD-160/rmd/r_r.siv"
-    "RIPEMD-160/rmd/s_l.fdl"
-    "RIPEMD-160/rmd/s_l.rls"
-    "RIPEMD-160/rmd/s_l.siv"
-    "RIPEMD-160/rmd/s_r.fdl"
-    "RIPEMD-160/rmd/s_r.rls"
-    "RIPEMD-160/rmd/s_r.siv"
 
 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   options [show_question_marks = false, spark_prv = false]
@@ -923,19 +886,6 @@
     VC_Principles
     Reference
     Complex_Types
-  files
-    "complex_types_app/initialize.fdl"
-    "complex_types_app/initialize.rls"
-    "complex_types_app/initialize.siv"
-    "loop_invariant/proc1.fdl"
-    "loop_invariant/proc1.rls"
-    "loop_invariant/proc1.siv"
-    "loop_invariant/proc2.fdl"
-    "loop_invariant/proc2.rls"
-    "loop_invariant/proc2.siv"
-    "simple_greatest_common_divisor/g_c_d.fdl"
-    "simple_greatest_common_divisor/g_c_d.rls"
-    "simple_greatest_common_divisor/g_c_d.siv"
   document_files
     "complex_types.ads"
     "complex_types_app.adb"