src/HOL/ROOT
changeset 56781 f2eb0f22589f
parent 56680 4e2a0d4e7a82
child 56801 8dd9df88f647
     1.1 --- a/src/HOL/ROOT	Tue Apr 29 12:00:50 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Tue Apr 29 13:29:05 2014 +0200
     1.3 @@ -9,8 +9,9 @@
     1.4    files
     1.5      "Tools/Quickcheck/Narrowing_Engine.hs"
     1.6      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     1.7 -    "document/root.bib"
     1.8 -    "document/root.tex"
     1.9 +  document_files
    1.10 +    "root.bib"
    1.11 +    "root.tex"
    1.12  
    1.13  session "HOL-Proofs" = Pure +
    1.14    description {*
    1.15 @@ -51,7 +52,7 @@
    1.16      Old_Recdef
    1.17    theories [condition = ISABELLE_FULL_TEST]
    1.18      Sum_of_Squares_Remote
    1.19 -  files "document/root.bib" "document/root.tex"
    1.20 +  document_files "root.bib" "root.tex"
    1.21  
    1.22  session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
    1.23    description {*
    1.24 @@ -73,7 +74,7 @@
    1.25    *}
    1.26    options [document_graph]
    1.27    theories Hahn_Banach
    1.28 -  files "document/root.bib" "document/root.tex"
    1.29 +  document_files "root.bib" "root.tex"
    1.30  
    1.31  session "HOL-Induct" in Induct = HOL +
    1.32    description {*
    1.33 @@ -106,7 +107,7 @@
    1.34      Comb
    1.35      PropLog
    1.36      Com
    1.37 -  files "document/root.tex"
    1.38 +  document_files "root.tex"
    1.39  
    1.40  session "HOL-IMP" in IMP = HOL +
    1.41    options [document_graph, document_variants=document]
    1.42 @@ -149,7 +150,7 @@
    1.43      Procs_Stat_Vars_Stat
    1.44      C_like
    1.45      OO
    1.46 -  files "document/root.bib" "document/root.tex"
    1.47 +  document_files "root.bib" "root.tex"
    1.48  
    1.49  session "HOL-IMPP" in IMPP = HOL +
    1.50    description {*
    1.51 @@ -185,8 +186,8 @@
    1.52      Pocklington
    1.53      Gauss
    1.54      Number_Theory
    1.55 -  files
    1.56 -    "document/root.tex"
    1.57 +  document_files
    1.58 +    "root.tex"
    1.59  
    1.60  session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
    1.61    description {*
    1.62 @@ -206,7 +207,7 @@
    1.63      Quadratic_Reciprocity
    1.64      Primes
    1.65      Pocklington
    1.66 -  files "document/root.tex"
    1.67 +  document_files "root.tex"
    1.68  
    1.69  session "HOL-Hoare" in Hoare = HOL +
    1.70    description {*
    1.71 @@ -214,7 +215,7 @@
    1.72      automatically from pre/post conditions and loop invariants).
    1.73    *}
    1.74    theories Hoare
    1.75 -  files "document/root.bib" "document/root.tex"
    1.76 +  document_files "root.bib" "root.tex"
    1.77  
    1.78  session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
    1.79    description {*
    1.80 @@ -223,7 +224,7 @@
    1.81    *}
    1.82    options [document_graph]
    1.83    theories Hoare_Parallel
    1.84 -  files "document/root.bib" "document/root.tex"
    1.85 +  document_files "root.bib" "root.tex"
    1.86  
    1.87  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
    1.88    options [document = false, document_graph = false, browser_info = false]
    1.89 @@ -285,7 +286,7 @@
    1.90      Divisibility         (* Rings *)
    1.91      IntRing              (* Ideals and residue classes *)
    1.92      UnivPoly             (* Polynomials *)
    1.93 -  files "document/root.bib" "document/root.tex"
    1.94 +  document_files "root.bib" "root.tex"
    1.95  
    1.96  session "HOL-Auth" in Auth = HOL +
    1.97    description {*
    1.98 @@ -298,7 +299,7 @@
    1.99      "Smartcard/Auth_Smartcard"
   1.100      "Guard/Auth_Guard_Shared"
   1.101      "Guard/Auth_Guard_Public"
   1.102 -  files "document/root.tex"
   1.103 +  document_files "root.tex"
   1.104  
   1.105  session "HOL-UNITY" in UNITY = "HOL-Auth" +
   1.106    description {*
   1.107 @@ -343,16 +344,16 @@
   1.108  
   1.109      (*obsolete*)
   1.110      "ELT"
   1.111 -  files "document/root.tex"
   1.112 +  document_files "root.tex"
   1.113  
   1.114  session "HOL-Unix" in Unix = HOL +
   1.115    options [print_mode = "no_brackets,no_type_brackets"]
   1.116    theories Unix
   1.117 -  files "document/root.bib" "document/root.tex"
   1.118 +  document_files "root.bib" "root.tex"
   1.119  
   1.120  session "HOL-ZF" in ZF = HOL +
   1.121    theories MainZF Games
   1.122 -  files "document/root.tex"
   1.123 +  document_files "root.tex"
   1.124  
   1.125  session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   1.126    options [document_graph, print_mode = "iff,no_brackets"]
   1.127 @@ -361,7 +362,7 @@
   1.128      "~~/src/HOL/Library/Monad_Syntax"
   1.129      "~~/src/HOL/Library/LaTeXsugar"
   1.130    theories Imperative_HOL_ex
   1.131 -  files "document/root.bib" "document/root.tex"
   1.132 +  document_files "root.bib" "root.tex"
   1.133  
   1.134  session "HOL-Decision_Procs" in Decision_Procs = HOL +
   1.135    description {*
   1.136 @@ -393,7 +394,7 @@
   1.137      Higman_Extraction
   1.138      Pigeonhole
   1.139      Euclid
   1.140 -  files "document/root.bib" "document/root.tex"
   1.141 +  document_files "root.bib" "root.tex"
   1.142  
   1.143  session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   1.144    description {*
   1.145 @@ -413,7 +414,7 @@
   1.146      StrongNorm
   1.147      Standardization
   1.148      WeakNorm
   1.149 -  files "document/root.bib" "document/root.tex"
   1.150 +  document_files "root.bib" "root.tex"
   1.151  
   1.152  session "HOL-Prolog" in Prolog = HOL +
   1.153    description {*
   1.154 @@ -437,10 +438,10 @@
   1.155    options [document_graph]
   1.156    theories [document = false] "~~/src/HOL/Library/While_Combinator"
   1.157    theories MicroJava
   1.158 -  files
   1.159 -    "document/introduction.tex"
   1.160 -    "document/root.bib"
   1.161 -    "document/root.tex"
   1.162 +  document_files
   1.163 +    "introduction.tex"
   1.164 +    "root.bib"
   1.165 +    "root.tex"
   1.166  
   1.167  session "HOL-NanoJava" in NanoJava = HOL +
   1.168    description {*
   1.169 @@ -448,7 +449,7 @@
   1.170    *}
   1.171    options [document_graph]
   1.172    theories Example
   1.173 -  files "document/root.bib" "document/root.tex"
   1.174 +  document_files "root.bib" "root.tex"
   1.175  
   1.176  session "HOL-Bali" in Bali = HOL +
   1.177    options [document_graph]
   1.178 @@ -457,7 +458,7 @@
   1.179      AxSound
   1.180      AxCompl
   1.181      Trans
   1.182 -  files "document/root.tex"
   1.183 +  document_files "root.tex"
   1.184  
   1.185  session "HOL-IOA" in IOA = HOL +
   1.186    description {*
   1.187 @@ -497,7 +498,7 @@
   1.188      Basic theory of lattices and orders.
   1.189    *}
   1.190    theories CompleteLattice
   1.191 -  files "document/root.tex"
   1.192 +  document_files "root.tex"
   1.193  
   1.194  session "HOL-ex" in ex = HOL +
   1.195    description {*
   1.196 @@ -586,7 +587,7 @@
   1.197  (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   1.198      SAT_Examples
   1.199  *)
   1.200 -  files "document/root.bib" "document/root.tex"
   1.201 +  document_files "root.bib" "root.tex"
   1.202  
   1.203  session "HOL-Isar_Examples" in Isar_Examples = HOL +
   1.204    description {*
   1.205 @@ -611,10 +612,10 @@
   1.206      Peirce
   1.207      Puzzle
   1.208      Summation
   1.209 -  files
   1.210 -    "document/root.bib"
   1.211 -    "document/root.tex"
   1.212 -    "document/style.tex"
   1.213 +  document_files
   1.214 +    "root.bib"
   1.215 +    "root.tex"
   1.216 +    "style.tex"
   1.217  
   1.218  session "HOL-SET_Protocol" in SET_Protocol = HOL +
   1.219    description {*
   1.220 @@ -623,7 +624,7 @@
   1.221    options [document_graph]
   1.222    theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   1.223    theories SET_Protocol
   1.224 -  files "document/root.tex"
   1.225 +  document_files "root.tex"
   1.226  
   1.227  session "HOL-Matrix_LP" in Matrix_LP = HOL +
   1.228    description {*
   1.229 @@ -631,7 +632,7 @@
   1.230    *}
   1.231    options [document_graph]
   1.232    theories Cplex
   1.233 -  files "document/root.tex"
   1.234 +  document_files "root.tex"
   1.235  
   1.236  session "HOL-TLA" in TLA = HOL +
   1.237    description {*
   1.238 @@ -678,8 +679,8 @@
   1.239      Determinants
   1.240      PolyRoots
   1.241      Complex_Analysis_Basics
   1.242 -  files
   1.243 -    "document/root.tex"
   1.244 +  document_files
   1.245 +    "root.tex"
   1.246  
   1.247  session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   1.248    options [document_graph]
   1.249 @@ -691,7 +692,7 @@
   1.250      Probability
   1.251      "ex/Dining_Cryptographers"
   1.252      "ex/Koepf_Duermuth_Countermeasure"
   1.253 -  files "document/root.tex"
   1.254 +  document_files "root.tex"
   1.255  
   1.256  session "HOL-Nominal" (main) in Nominal = HOL +
   1.257    options [document = false]
   1.258 @@ -708,10 +709,10 @@
   1.259    *}
   1.260    options [document = false]
   1.261    theories Cardinals
   1.262 -  files
   1.263 -    "document/intro.tex"
   1.264 -    "document/root.tex"
   1.265 -    "document/root.bib"
   1.266 +  document_files
   1.267 +    "intro.tex"
   1.268 +    "root.tex"
   1.269 +    "root.bib"
   1.270  
   1.271  session "HOL-BNF_Examples" in BNF_Examples = HOL +
   1.272    description {*
   1.273 @@ -735,7 +736,7 @@
   1.274  session "HOL-Word" (main) in Word = HOL +
   1.275    options [document_graph]
   1.276    theories Word
   1.277 -  files "document/root.bib" "document/root.tex"
   1.278 +  document_files "root.bib" "root.tex"
   1.279  
   1.280  session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   1.281    options [document = false]
   1.282 @@ -744,7 +745,7 @@
   1.283  session "HOL-Statespace" in Statespace = HOL +
   1.284    theories [skip_proofs = false]
   1.285      StateSpaceEx
   1.286 -  files "document/root.tex"
   1.287 +  document_files "root.tex"
   1.288  
   1.289  session "HOL-NSA" in NSA = HOL +
   1.290    description {*
   1.291 @@ -752,7 +753,7 @@
   1.292    *}
   1.293    options [document_graph]
   1.294    theories Hypercomplex
   1.295 -  files "document/root.tex"
   1.296 +  document_files "root.tex"
   1.297  
   1.298  session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   1.299    options [document = false]
   1.300 @@ -850,18 +851,6 @@
   1.301      "complex_types_app/initialize.fdl"
   1.302      "complex_types_app/initialize.rls"
   1.303      "complex_types_app/initialize.siv"
   1.304 -    "document/complex_types.ads"
   1.305 -    "document/complex_types_app.adb"
   1.306 -    "document/complex_types_app.ads"
   1.307 -    "document/Gcd.adb"
   1.308 -    "document/Gcd.ads"
   1.309 -    "document/intro.tex"
   1.310 -    "document/loop_invariant.adb"
   1.311 -    "document/loop_invariant.ads"
   1.312 -    "document/root.bib"
   1.313 -    "document/root.tex"
   1.314 -    "document/Simple_Gcd.adb"
   1.315 -    "document/Simple_Gcd.ads"
   1.316      "loop_invariant/proc1.fdl"
   1.317      "loop_invariant/proc1.rls"
   1.318      "loop_invariant/proc1.siv"
   1.319 @@ -871,6 +860,19 @@
   1.320      "simple_greatest_common_divisor/g_c_d.fdl"
   1.321      "simple_greatest_common_divisor/g_c_d.rls"
   1.322      "simple_greatest_common_divisor/g_c_d.siv"
   1.323 +  document_files
   1.324 +    "complex_types.ads"
   1.325 +    "complex_types_app.adb"
   1.326 +    "complex_types_app.ads"
   1.327 +    "Gcd.adb"
   1.328 +    "Gcd.ads"
   1.329 +    "intro.tex"
   1.330 +    "loop_invariant.adb"
   1.331 +    "loop_invariant.ads"
   1.332 +    "root.bib"
   1.333 +    "root.tex"
   1.334 +    "Simple_Gcd.adb"
   1.335 +    "Simple_Gcd.ads"
   1.336  
   1.337  session "HOL-Mutabelle" in Mutabelle = HOL +
   1.338    options [document = false]
   1.339 @@ -950,14 +952,14 @@
   1.340      Plain_HOLCF
   1.341      Fixrec
   1.342      HOLCF
   1.343 -  files "document/root.tex"
   1.344 +  document_files "root.tex"
   1.345  
   1.346  session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   1.347    theories
   1.348      Domain_ex
   1.349      Fixrec_ex
   1.350      New_Domain
   1.351 -  files "document/root.tex"
   1.352 +  document_files "root.tex"
   1.353  
   1.354  session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   1.355    options [document = false]
   1.356 @@ -971,7 +973,7 @@
   1.357    *}
   1.358    options [document = false]
   1.359    theories HoareEx
   1.360 -  files "document/root.tex"
   1.361 +  document_files "root.tex"
   1.362  
   1.363  session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   1.364    description {*