clarified parent session images, to avoid duplicate loading of theories;
authorwenzelm
Mon Apr 24 11:52:51 2017 +0200 (2017-04-24)
changeset 655730f3fdf689bf9
parent 65572 6acb28e5ba41
child 65574 10f4a17e5928
clarified parent session images, to avoid duplicate loading of theories;
src/Benchmarks/ROOT
src/Doc/ROOT
src/HOL/ROOT
     1.1 --- a/src/Benchmarks/ROOT	Mon Apr 24 11:23:07 2017 +0200
     1.2 +++ b/src/Benchmarks/ROOT	Mon Apr 24 11:52:51 2017 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  chapter HOL
     1.5  
     1.6 -session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
     1.7 +session "HOL-Datatype_Benchmark" in Datatype_Benchmark = "HOL-Library" +
     1.8    description {*
     1.9      Big (co)datatypes.
    1.10    *}
    1.11 @@ -10,7 +10,7 @@
    1.12      IsaFoR
    1.13      Misc_N2M
    1.14  
    1.15 -session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
    1.16 +session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = "HOL-Library" +
    1.17    theories [quick_and_dirty]
    1.18      Find_Unused_Assms_Examples
    1.19      Needham_Schroeder_No_Attacker_Example
     2.1 --- a/src/Doc/ROOT	Mon Apr 24 11:23:07 2017 +0200
     2.2 +++ b/src/Doc/ROOT	Mon Apr 24 11:52:51 2017 +0200
     2.3 @@ -46,6 +46,8 @@
     2.4  
     2.5  session Corec (doc) in "Corec" = "HOL-Library" +
     2.6    options [document_variants = "corec"]
     2.7 +  sessions
     2.8 +    Datatypes
     2.9    theories [document = false] "../Datatypes/Setup"
    2.10    theories Corec
    2.11    document_files (in "..")
    2.12 @@ -170,7 +172,7 @@
    2.13      "root.tex"
    2.14      "style.sty"
    2.15  
    2.16 -session Isar_Ref (doc) in "Isar_Ref" = HOL +
    2.17 +session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" +
    2.18    options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
    2.19    theories
    2.20      Preface
    2.21 @@ -244,7 +246,9 @@
    2.22  
    2.23  session Sugar (doc) in "Sugar" = HOL +
    2.24    options [document_variants = "sugar"]
    2.25 -  theories [document = ""]
    2.26 +  sessions
    2.27 +    "HOL-Library"
    2.28 +  theories [document = false]
    2.29      "~~/src/HOL/Library/LaTeXsugar"
    2.30      "~~/src/HOL/Library/OptionalSugar"
    2.31    theories Sugar
    2.32 @@ -436,7 +440,7 @@
    2.33    theories
    2.34      "Protocol/NS_Public"
    2.35      "Documents/Documents"
    2.36 -  theories [document = ""]
    2.37 +  theories [document = false]
    2.38      "Types/Setup"
    2.39    theories [thy_output_margin = 64, thy_output_indent = 0]
    2.40      "Types/Numbers"
    2.41 @@ -502,7 +506,7 @@
    2.42      "root.tex"
    2.43      "style.sty"
    2.44  
    2.45 -session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" +
    2.46 +session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
    2.47    options [document = false]
    2.48    theories
    2.49      Setup
     3.1 --- a/src/HOL/ROOT	Mon Apr 24 11:23:07 2017 +0200
     3.2 +++ b/src/HOL/ROOT	Mon Apr 24 11:52:51 2017 +0200
     3.3 @@ -96,6 +96,8 @@
     3.4      subspaces (not only one-dimensional subspaces), can be extended to a
     3.5      continous linearform on the whole vectorspace.
     3.6    *}
     3.7 +  sessions
     3.8 +    "HOL-Analysis"
     3.9    theories
    3.10      Hahn_Banach
    3.11    document_files "root.bib" "root.tex"
    3.12 @@ -136,7 +138,7 @@
    3.13      Com
    3.14    document_files "root.tex"
    3.15  
    3.16 -session "HOL-IMP" (timing) in IMP = HOL +
    3.17 +session "HOL-IMP" (timing) in IMP = "HOL-Library" +
    3.18    options [document_variants = document]
    3.19    theories [document = false]
    3.20      "~~/src/HOL/Library/While_Combinator"
    3.21 @@ -192,6 +194,8 @@
    3.22  
    3.23  session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
    3.24    options [document_variants = document]
    3.25 +  sessions
    3.26 +    "HOL-Number_Theory"
    3.27    theories [document = false]
    3.28      Less_False
    3.29      "~~/src/HOL/Library/Multiset"
    3.30 @@ -248,6 +252,9 @@
    3.31  
    3.32  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" +
    3.33    options [document = false, browser_info = false]
    3.34 +  sessions
    3.35 +    "HOL-Data_Structures"
    3.36 +    "HOL-ex"
    3.37    theories
    3.38      Generate
    3.39      Generate_Binary_Nat
    3.40 @@ -265,7 +272,7 @@
    3.41    theories [condition = "ISABELLE_SMLNJ"]
    3.42      Code_Test_SMLNJ
    3.43  
    3.44 -session "HOL-Metis_Examples" (timing) in Metis_Examples = HOL +
    3.45 +session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
    3.46    description {*
    3.47      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.48      Author:     Jasmin Blanchette, TU Muenchen
    3.49 @@ -273,6 +280,8 @@
    3.50      Testing Metis and Sledgehammer.
    3.51    *}
    3.52    options [document = false]
    3.53 +  sessions
    3.54 +    "HOL-Decision_Procs"
    3.55    theories
    3.56      Abstraction
    3.57      Big_O
    3.58 @@ -284,7 +293,7 @@
    3.59      Trans_Closure
    3.60      Sets
    3.61  
    3.62 -session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
    3.63 +session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" +
    3.64    description {*
    3.65      Author:     Jasmin Blanchette, TU Muenchen
    3.66      Copyright   2009
    3.67 @@ -332,7 +341,7 @@
    3.68      More_Ring
    3.69    document_files "root.bib" "root.tex"
    3.70  
    3.71 -session "HOL-Auth" (timing) in Auth = HOL +
    3.72 +session "HOL-Auth" (timing) in Auth = "HOL-Library" +
    3.73    description {*
    3.74      A new approach to verifying authentication protocols.
    3.75    *}
    3.76 @@ -388,13 +397,15 @@
    3.77      ELT
    3.78    document_files "root.tex"
    3.79  
    3.80 -session "HOL-Unix" in Unix = HOL +
    3.81 +session "HOL-Unix" in Unix = "HOL-Library" +
    3.82    options [print_mode = "no_brackets,no_type_brackets"]
    3.83    theories Unix
    3.84    document_files "root.bib" "root.tex"
    3.85  
    3.86 -session "HOL-ZF" in ZF = HOL +
    3.87 -  theories MainZF Games
    3.88 +session "HOL-ZF" in ZF = "HOL-Library" +
    3.89 +  theories
    3.90 +    MainZF
    3.91 +    Games
    3.92    document_files "root.tex"
    3.93  
    3.94  session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
    3.95 @@ -416,6 +427,8 @@
    3.96  
    3.97  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    3.98    options [document = false]
    3.99 +  sessions
   3.100 +    "HOL-Isar_Examples"
   3.101    theories
   3.102      Hilbert_Classical
   3.103      Proof_Terms
   3.104 @@ -482,6 +495,8 @@
   3.105      machine and a specification of its bytecode verifier and a lightweight
   3.106      bytecode verifier, including proofs of type-safety.
   3.107    *}
   3.108 +  sessions
   3.109 +    "HOL-Eisbach"
   3.110    theories [document = false]
   3.111      "~~/src/HOL/Library/While_Combinator"
   3.112    theories
   3.113 @@ -498,7 +513,7 @@
   3.114    theories Example
   3.115    document_files "root.bib" "root.tex"
   3.116  
   3.117 -session "HOL-Bali" (timing) in Bali = HOL +
   3.118 +session "HOL-Bali" (timing) in Bali = "HOL-Library" +
   3.119    theories
   3.120      AxExample
   3.121      AxSound
   3.122 @@ -716,7 +731,7 @@
   3.123    options [document = false]
   3.124    theories MemoryImplementation
   3.125  
   3.126 -session "HOL-TPTP" in TPTP = HOL +
   3.127 +session "HOL-TPTP" in TPTP = "HOL-Library" +
   3.128    description {*
   3.129      Author:     Jasmin Blanchette, TU Muenchen
   3.130      Author:     Nik Sultana, University of Cambridge
   3.131 @@ -753,7 +768,10 @@
   3.132  
   3.133  session "HOL-Nominal" in Nominal = HOL +
   3.134    options [document = false]
   3.135 -  theories Nominal
   3.136 +  sessions
   3.137 +    "HOL-Library"
   3.138 +  theories
   3.139 +    Nominal
   3.140  
   3.141  session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   3.142    options [document = false]
   3.143 @@ -781,7 +799,7 @@
   3.144    theories [quick_and_dirty]
   3.145      VC_Condition
   3.146  
   3.147 -session "HOL-Cardinals" (timing) in Cardinals = HOL +
   3.148 +session "HOL-Cardinals" (timing) in Cardinals = "HOL-Library" +
   3.149    description {*
   3.150      Ordinals and Cardinals, Full Theories.
   3.151    *}
   3.152 @@ -799,6 +817,8 @@
   3.153      (Co)datatype Examples.
   3.154    *}
   3.155    options [document = false]
   3.156 +  sessions
   3.157 +    "HOL-Library"
   3.158    theories
   3.159      Compat
   3.160      Lambda_Term
   3.161 @@ -815,7 +835,7 @@
   3.162      Misc_Primcorec
   3.163      Misc_Primrec
   3.164  
   3.165 -session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL +
   3.166 +session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   3.167    description {*
   3.168      Corecursion Examples.
   3.169    *}
   3.170 @@ -838,6 +858,8 @@
   3.171      "Tests/Type_Class"
   3.172  
   3.173  session "HOL-Word" (main timing) in Word = HOL +
   3.174 +  sessions
   3.175 +    "HOL-Library"
   3.176    theories
   3.177      Word
   3.178    document_files "root.bib" "root.tex"
   3.179 @@ -944,7 +966,7 @@
   3.180      "RIPEMD-160/rmd/s_r.rls"
   3.181      "RIPEMD-160/rmd/s_r.siv"
   3.182  
   3.183 -session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   3.184 +session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK-Examples" +
   3.185    options [show_question_marks = false, spark_prv = false]
   3.186    theories
   3.187      Example_Verification
   3.188 @@ -978,7 +1000,7 @@
   3.189      "Simple_Gcd.adb"
   3.190      "Simple_Gcd.ads"
   3.191  
   3.192 -session "HOL-Mutabelle" in Mutabelle = HOL +
   3.193 +session "HOL-Mutabelle" in Mutabelle = "HOL-Library" +
   3.194    options [document = false]
   3.195    theories MutabelleExtra
   3.196  
   3.197 @@ -1081,10 +1103,13 @@
   3.198      This is the HOLCF-based denotational semantics of a simple WHILE-language.
   3.199    *}
   3.200    options [document = false]
   3.201 -  theories HoareEx
   3.202 +  sessions
   3.203 +    "HOL-IMP"
   3.204 +  theories
   3.205 +    HoareEx
   3.206    document_files "root.tex"
   3.207  
   3.208 -session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   3.209 +session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   3.210    description {*
   3.211      Miscellaneous examples for HOLCF.
   3.212    *}
   3.213 @@ -1102,7 +1127,7 @@
   3.214      Letrec
   3.215      Pattern_Match
   3.216  
   3.217 -session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   3.218 +session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
   3.219    description {*
   3.220      FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
   3.221