removed pointless dependencies: done by 'spark_open';
authorwenzelm
Mon Oct 02 18:11:28 2017 +0200 (18 months ago)
changeset 667551ceedf710564
parent 66754 78c74f9e960a
child 66756 a1b2ea991ad1
removed pointless dependencies: done by 'spark_open';
src/HOL/ROOT
     1.1 --- a/src/HOL/ROOT	Mon Oct 02 16:47:46 2017 +0200
     1.2 +++ b/src/HOL/ROOT	Mon Oct 02 18:11:28 2017 +0200
     1.3 @@ -865,9 +865,7 @@
     1.4    options [document = false, spark_prv = false]
     1.5    theories
     1.6      "Gcd/Greatest_Common_Divisor"
     1.7 -
     1.8      "Liseq/Longest_Increasing_Subsequence"
     1.9 -
    1.10      "RIPEMD-160/F"
    1.11      "RIPEMD-160/Hash"
    1.12      "RIPEMD-160/K_L"
    1.13 @@ -877,42 +875,7 @@
    1.14      "RIPEMD-160/R_R"
    1.15      "RIPEMD-160/S_L"
    1.16      "RIPEMD-160/S_R"
    1.17 -
    1.18      "Sqrt/Sqrt"
    1.19 -  files
    1.20 -    "Gcd/greatest_common_divisor/g_c_d.fdl"
    1.21 -    "Gcd/greatest_common_divisor/g_c_d.rls"
    1.22 -    "Gcd/greatest_common_divisor/g_c_d.siv"
    1.23 -    "Liseq/liseq/liseq_length.fdl"
    1.24 -    "Liseq/liseq/liseq_length.rls"
    1.25 -    "Liseq/liseq/liseq_length.siv"
    1.26 -    "RIPEMD-160/rmd/f.fdl"
    1.27 -    "RIPEMD-160/rmd/f.rls"
    1.28 -    "RIPEMD-160/rmd/f.siv"
    1.29 -    "RIPEMD-160/rmd/hash.fdl"
    1.30 -    "RIPEMD-160/rmd/hash.rls"
    1.31 -    "RIPEMD-160/rmd/hash.siv"
    1.32 -    "RIPEMD-160/rmd/k_l.fdl"
    1.33 -    "RIPEMD-160/rmd/k_l.rls"
    1.34 -    "RIPEMD-160/rmd/k_l.siv"
    1.35 -    "RIPEMD-160/rmd/k_r.fdl"
    1.36 -    "RIPEMD-160/rmd/k_r.rls"
    1.37 -    "RIPEMD-160/rmd/k_r.siv"
    1.38 -    "RIPEMD-160/rmd/r_l.fdl"
    1.39 -    "RIPEMD-160/rmd/r_l.rls"
    1.40 -    "RIPEMD-160/rmd/r_l.siv"
    1.41 -    "RIPEMD-160/rmd/round.fdl"
    1.42 -    "RIPEMD-160/rmd/round.rls"
    1.43 -    "RIPEMD-160/rmd/round.siv"
    1.44 -    "RIPEMD-160/rmd/r_r.fdl"
    1.45 -    "RIPEMD-160/rmd/r_r.rls"
    1.46 -    "RIPEMD-160/rmd/r_r.siv"
    1.47 -    "RIPEMD-160/rmd/s_l.fdl"
    1.48 -    "RIPEMD-160/rmd/s_l.rls"
    1.49 -    "RIPEMD-160/rmd/s_l.siv"
    1.50 -    "RIPEMD-160/rmd/s_r.fdl"
    1.51 -    "RIPEMD-160/rmd/s_r.rls"
    1.52 -    "RIPEMD-160/rmd/s_r.siv"
    1.53  
    1.54  session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
    1.55    options [show_question_marks = false, spark_prv = false]
    1.56 @@ -923,19 +886,6 @@
    1.57      VC_Principles
    1.58      Reference
    1.59      Complex_Types
    1.60 -  files
    1.61 -    "complex_types_app/initialize.fdl"
    1.62 -    "complex_types_app/initialize.rls"
    1.63 -    "complex_types_app/initialize.siv"
    1.64 -    "loop_invariant/proc1.fdl"
    1.65 -    "loop_invariant/proc1.rls"
    1.66 -    "loop_invariant/proc1.siv"
    1.67 -    "loop_invariant/proc2.fdl"
    1.68 -    "loop_invariant/proc2.rls"
    1.69 -    "loop_invariant/proc2.siv"
    1.70 -    "simple_greatest_common_divisor/g_c_d.fdl"
    1.71 -    "simple_greatest_common_divisor/g_c_d.rls"
    1.72 -    "simple_greatest_common_divisor/g_c_d.siv"
    1.73    document_files
    1.74      "complex_types.ads"
    1.75      "complex_types_app.adb"