systematic replacement of 'files' by 'document_files';
authorwenzelm
Tue Apr 29 13:29:05 2014 +0200 (2014-04-29)
changeset 56781f2eb0f22589f
parent 56780 e76467fed375
child 56782 433cf57550fa
systematic replacement of 'files' by 'document_files';
src/FOL/ROOT
src/HOL/ROOT
src/ZF/ROOT
     1.1 --- a/src/FOL/ROOT	Tue Apr 29 12:00:50 2014 +0200
     1.2 +++ b/src/FOL/ROOT	Tue Apr 29 13:29:05 2014 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4      Michael Dummett, Elements of Intuitionism (Oxford, 1977)
     1.5    *}
     1.6    theories FOL
     1.7 -  files "document/root.tex"
     1.8 +  document_files "root.tex"
     1.9  
    1.10  session "FOL-ex" in ex = FOL +
    1.11    description {*
    1.12 @@ -40,5 +40,5 @@
    1.13      If
    1.14    theories [document = false, skip_proofs = false]
    1.15      "Locale_Test/Locale_Test"
    1.16 -  files "document/root.tex"
    1.17 +  document_files "root.tex"
    1.18  
     2.1 --- a/src/HOL/ROOT	Tue Apr 29 12:00:50 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Apr 29 13:29:05 2014 +0200
     2.3 @@ -9,8 +9,9 @@
     2.4    files
     2.5      "Tools/Quickcheck/Narrowing_Engine.hs"
     2.6      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     2.7 -    "document/root.bib"
     2.8 -    "document/root.tex"
     2.9 +  document_files
    2.10 +    "root.bib"
    2.11 +    "root.tex"
    2.12  
    2.13  session "HOL-Proofs" = Pure +
    2.14    description {*
    2.15 @@ -51,7 +52,7 @@
    2.16      Old_Recdef
    2.17    theories [condition = ISABELLE_FULL_TEST]
    2.18      Sum_of_Squares_Remote
    2.19 -  files "document/root.bib" "document/root.tex"
    2.20 +  document_files "root.bib" "root.tex"
    2.21  
    2.22  session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
    2.23    description {*
    2.24 @@ -73,7 +74,7 @@
    2.25    *}
    2.26    options [document_graph]
    2.27    theories Hahn_Banach
    2.28 -  files "document/root.bib" "document/root.tex"
    2.29 +  document_files "root.bib" "root.tex"
    2.30  
    2.31  session "HOL-Induct" in Induct = HOL +
    2.32    description {*
    2.33 @@ -106,7 +107,7 @@
    2.34      Comb
    2.35      PropLog
    2.36      Com
    2.37 -  files "document/root.tex"
    2.38 +  document_files "root.tex"
    2.39  
    2.40  session "HOL-IMP" in IMP = HOL +
    2.41    options [document_graph, document_variants=document]
    2.42 @@ -149,7 +150,7 @@
    2.43      Procs_Stat_Vars_Stat
    2.44      C_like
    2.45      OO
    2.46 -  files "document/root.bib" "document/root.tex"
    2.47 +  document_files "root.bib" "root.tex"
    2.48  
    2.49  session "HOL-IMPP" in IMPP = HOL +
    2.50    description {*
    2.51 @@ -185,8 +186,8 @@
    2.52      Pocklington
    2.53      Gauss
    2.54      Number_Theory
    2.55 -  files
    2.56 -    "document/root.tex"
    2.57 +  document_files
    2.58 +    "root.tex"
    2.59  
    2.60  session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
    2.61    description {*
    2.62 @@ -206,7 +207,7 @@
    2.63      Quadratic_Reciprocity
    2.64      Primes
    2.65      Pocklington
    2.66 -  files "document/root.tex"
    2.67 +  document_files "root.tex"
    2.68  
    2.69  session "HOL-Hoare" in Hoare = HOL +
    2.70    description {*
    2.71 @@ -214,7 +215,7 @@
    2.72      automatically from pre/post conditions and loop invariants).
    2.73    *}
    2.74    theories Hoare
    2.75 -  files "document/root.bib" "document/root.tex"
    2.76 +  document_files "root.bib" "root.tex"
    2.77  
    2.78  session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
    2.79    description {*
    2.80 @@ -223,7 +224,7 @@
    2.81    *}
    2.82    options [document_graph]
    2.83    theories Hoare_Parallel
    2.84 -  files "document/root.bib" "document/root.tex"
    2.85 +  document_files "root.bib" "root.tex"
    2.86  
    2.87  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
    2.88    options [document = false, document_graph = false, browser_info = false]
    2.89 @@ -285,7 +286,7 @@
    2.90      Divisibility         (* Rings *)
    2.91      IntRing              (* Ideals and residue classes *)
    2.92      UnivPoly             (* Polynomials *)
    2.93 -  files "document/root.bib" "document/root.tex"
    2.94 +  document_files "root.bib" "root.tex"
    2.95  
    2.96  session "HOL-Auth" in Auth = HOL +
    2.97    description {*
    2.98 @@ -298,7 +299,7 @@
    2.99      "Smartcard/Auth_Smartcard"
   2.100      "Guard/Auth_Guard_Shared"
   2.101      "Guard/Auth_Guard_Public"
   2.102 -  files "document/root.tex"
   2.103 +  document_files "root.tex"
   2.104  
   2.105  session "HOL-UNITY" in UNITY = "HOL-Auth" +
   2.106    description {*
   2.107 @@ -343,16 +344,16 @@
   2.108  
   2.109      (*obsolete*)
   2.110      "ELT"
   2.111 -  files "document/root.tex"
   2.112 +  document_files "root.tex"
   2.113  
   2.114  session "HOL-Unix" in Unix = HOL +
   2.115    options [print_mode = "no_brackets,no_type_brackets"]
   2.116    theories Unix
   2.117 -  files "document/root.bib" "document/root.tex"
   2.118 +  document_files "root.bib" "root.tex"
   2.119  
   2.120  session "HOL-ZF" in ZF = HOL +
   2.121    theories MainZF Games
   2.122 -  files "document/root.tex"
   2.123 +  document_files "root.tex"
   2.124  
   2.125  session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   2.126    options [document_graph, print_mode = "iff,no_brackets"]
   2.127 @@ -361,7 +362,7 @@
   2.128      "~~/src/HOL/Library/Monad_Syntax"
   2.129      "~~/src/HOL/Library/LaTeXsugar"
   2.130    theories Imperative_HOL_ex
   2.131 -  files "document/root.bib" "document/root.tex"
   2.132 +  document_files "root.bib" "root.tex"
   2.133  
   2.134  session "HOL-Decision_Procs" in Decision_Procs = HOL +
   2.135    description {*
   2.136 @@ -393,7 +394,7 @@
   2.137      Higman_Extraction
   2.138      Pigeonhole
   2.139      Euclid
   2.140 -  files "document/root.bib" "document/root.tex"
   2.141 +  document_files "root.bib" "root.tex"
   2.142  
   2.143  session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   2.144    description {*
   2.145 @@ -413,7 +414,7 @@
   2.146      StrongNorm
   2.147      Standardization
   2.148      WeakNorm
   2.149 -  files "document/root.bib" "document/root.tex"
   2.150 +  document_files "root.bib" "root.tex"
   2.151  
   2.152  session "HOL-Prolog" in Prolog = HOL +
   2.153    description {*
   2.154 @@ -437,10 +438,10 @@
   2.155    options [document_graph]
   2.156    theories [document = false] "~~/src/HOL/Library/While_Combinator"
   2.157    theories MicroJava
   2.158 -  files
   2.159 -    "document/introduction.tex"
   2.160 -    "document/root.bib"
   2.161 -    "document/root.tex"
   2.162 +  document_files
   2.163 +    "introduction.tex"
   2.164 +    "root.bib"
   2.165 +    "root.tex"
   2.166  
   2.167  session "HOL-NanoJava" in NanoJava = HOL +
   2.168    description {*
   2.169 @@ -448,7 +449,7 @@
   2.170    *}
   2.171    options [document_graph]
   2.172    theories Example
   2.173 -  files "document/root.bib" "document/root.tex"
   2.174 +  document_files "root.bib" "root.tex"
   2.175  
   2.176  session "HOL-Bali" in Bali = HOL +
   2.177    options [document_graph]
   2.178 @@ -457,7 +458,7 @@
   2.179      AxSound
   2.180      AxCompl
   2.181      Trans
   2.182 -  files "document/root.tex"
   2.183 +  document_files "root.tex"
   2.184  
   2.185  session "HOL-IOA" in IOA = HOL +
   2.186    description {*
   2.187 @@ -497,7 +498,7 @@
   2.188      Basic theory of lattices and orders.
   2.189    *}
   2.190    theories CompleteLattice
   2.191 -  files "document/root.tex"
   2.192 +  document_files "root.tex"
   2.193  
   2.194  session "HOL-ex" in ex = HOL +
   2.195    description {*
   2.196 @@ -586,7 +587,7 @@
   2.197  (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   2.198      SAT_Examples
   2.199  *)
   2.200 -  files "document/root.bib" "document/root.tex"
   2.201 +  document_files "root.bib" "root.tex"
   2.202  
   2.203  session "HOL-Isar_Examples" in Isar_Examples = HOL +
   2.204    description {*
   2.205 @@ -611,10 +612,10 @@
   2.206      Peirce
   2.207      Puzzle
   2.208      Summation
   2.209 -  files
   2.210 -    "document/root.bib"
   2.211 -    "document/root.tex"
   2.212 -    "document/style.tex"
   2.213 +  document_files
   2.214 +    "root.bib"
   2.215 +    "root.tex"
   2.216 +    "style.tex"
   2.217  
   2.218  session "HOL-SET_Protocol" in SET_Protocol = HOL +
   2.219    description {*
   2.220 @@ -623,7 +624,7 @@
   2.221    options [document_graph]
   2.222    theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   2.223    theories SET_Protocol
   2.224 -  files "document/root.tex"
   2.225 +  document_files "root.tex"
   2.226  
   2.227  session "HOL-Matrix_LP" in Matrix_LP = HOL +
   2.228    description {*
   2.229 @@ -631,7 +632,7 @@
   2.230    *}
   2.231    options [document_graph]
   2.232    theories Cplex
   2.233 -  files "document/root.tex"
   2.234 +  document_files "root.tex"
   2.235  
   2.236  session "HOL-TLA" in TLA = HOL +
   2.237    description {*
   2.238 @@ -678,8 +679,8 @@
   2.239      Determinants
   2.240      PolyRoots
   2.241      Complex_Analysis_Basics
   2.242 -  files
   2.243 -    "document/root.tex"
   2.244 +  document_files
   2.245 +    "root.tex"
   2.246  
   2.247  session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   2.248    options [document_graph]
   2.249 @@ -691,7 +692,7 @@
   2.250      Probability
   2.251      "ex/Dining_Cryptographers"
   2.252      "ex/Koepf_Duermuth_Countermeasure"
   2.253 -  files "document/root.tex"
   2.254 +  document_files "root.tex"
   2.255  
   2.256  session "HOL-Nominal" (main) in Nominal = HOL +
   2.257    options [document = false]
   2.258 @@ -708,10 +709,10 @@
   2.259    *}
   2.260    options [document = false]
   2.261    theories Cardinals
   2.262 -  files
   2.263 -    "document/intro.tex"
   2.264 -    "document/root.tex"
   2.265 -    "document/root.bib"
   2.266 +  document_files
   2.267 +    "intro.tex"
   2.268 +    "root.tex"
   2.269 +    "root.bib"
   2.270  
   2.271  session "HOL-BNF_Examples" in BNF_Examples = HOL +
   2.272    description {*
   2.273 @@ -735,7 +736,7 @@
   2.274  session "HOL-Word" (main) in Word = HOL +
   2.275    options [document_graph]
   2.276    theories Word
   2.277 -  files "document/root.bib" "document/root.tex"
   2.278 +  document_files "root.bib" "root.tex"
   2.279  
   2.280  session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   2.281    options [document = false]
   2.282 @@ -744,7 +745,7 @@
   2.283  session "HOL-Statespace" in Statespace = HOL +
   2.284    theories [skip_proofs = false]
   2.285      StateSpaceEx
   2.286 -  files "document/root.tex"
   2.287 +  document_files "root.tex"
   2.288  
   2.289  session "HOL-NSA" in NSA = HOL +
   2.290    description {*
   2.291 @@ -752,7 +753,7 @@
   2.292    *}
   2.293    options [document_graph]
   2.294    theories Hypercomplex
   2.295 -  files "document/root.tex"
   2.296 +  document_files "root.tex"
   2.297  
   2.298  session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   2.299    options [document = false]
   2.300 @@ -850,18 +851,6 @@
   2.301      "complex_types_app/initialize.fdl"
   2.302      "complex_types_app/initialize.rls"
   2.303      "complex_types_app/initialize.siv"
   2.304 -    "document/complex_types.ads"
   2.305 -    "document/complex_types_app.adb"
   2.306 -    "document/complex_types_app.ads"
   2.307 -    "document/Gcd.adb"
   2.308 -    "document/Gcd.ads"
   2.309 -    "document/intro.tex"
   2.310 -    "document/loop_invariant.adb"
   2.311 -    "document/loop_invariant.ads"
   2.312 -    "document/root.bib"
   2.313 -    "document/root.tex"
   2.314 -    "document/Simple_Gcd.adb"
   2.315 -    "document/Simple_Gcd.ads"
   2.316      "loop_invariant/proc1.fdl"
   2.317      "loop_invariant/proc1.rls"
   2.318      "loop_invariant/proc1.siv"
   2.319 @@ -871,6 +860,19 @@
   2.320      "simple_greatest_common_divisor/g_c_d.fdl"
   2.321      "simple_greatest_common_divisor/g_c_d.rls"
   2.322      "simple_greatest_common_divisor/g_c_d.siv"
   2.323 +  document_files
   2.324 +    "complex_types.ads"
   2.325 +    "complex_types_app.adb"
   2.326 +    "complex_types_app.ads"
   2.327 +    "Gcd.adb"
   2.328 +    "Gcd.ads"
   2.329 +    "intro.tex"
   2.330 +    "loop_invariant.adb"
   2.331 +    "loop_invariant.ads"
   2.332 +    "root.bib"
   2.333 +    "root.tex"
   2.334 +    "Simple_Gcd.adb"
   2.335 +    "Simple_Gcd.ads"
   2.336  
   2.337  session "HOL-Mutabelle" in Mutabelle = HOL +
   2.338    options [document = false]
   2.339 @@ -950,14 +952,14 @@
   2.340      Plain_HOLCF
   2.341      Fixrec
   2.342      HOLCF
   2.343 -  files "document/root.tex"
   2.344 +  document_files "root.tex"
   2.345  
   2.346  session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   2.347    theories
   2.348      Domain_ex
   2.349      Fixrec_ex
   2.350      New_Domain
   2.351 -  files "document/root.tex"
   2.352 +  document_files "root.tex"
   2.353  
   2.354  session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   2.355    options [document = false]
   2.356 @@ -971,7 +973,7 @@
   2.357    *}
   2.358    options [document = false]
   2.359    theories HoareEx
   2.360 -  files "document/root.tex"
   2.361 +  document_files "root.tex"
   2.362  
   2.363  session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   2.364    description {*
     3.1 --- a/src/ZF/ROOT	Tue Apr 29 12:00:50 2014 +0200
     3.2 +++ b/src/ZF/ROOT	Tue Apr 29 13:29:05 2014 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4    theories
     3.5      Main
     3.6      Main_ZFC
     3.7 -  files "document/root.tex"
     3.8 +  document_files "root.tex"
     3.9  
    3.10  session "ZF-AC" in AC = ZF +
    3.11    description {*
    3.12 @@ -75,7 +75,7 @@
    3.13      AC17_AC1
    3.14      AC18_AC19
    3.15      DC
    3.16 -  files "document/root.tex" "document/root.bib"
    3.17 +  document_files "root.tex" "root.bib"
    3.18  
    3.19  session "ZF-Coind" in Coind = ZF +
    3.20    description {*
    3.21 @@ -125,7 +125,7 @@
    3.22    *}
    3.23    options [document_graph]
    3.24    theories DPow_absolute AC_in_L Rank_Separation
    3.25 -  files "document/root.tex" "document/root.bib"
    3.26 +  document_files "root.tex" "root.bib"
    3.27  
    3.28  session "ZF-IMP" in IMP = ZF +
    3.29    description {*
    3.30 @@ -143,7 +143,7 @@
    3.31    *}
    3.32    options [document = false]
    3.33    theories Equiv
    3.34 -  files "document/root.tex" "document/root.bib"
    3.35 +  document_files "root.tex" "root.bib"
    3.36  
    3.37  session "ZF-Induct" in Induct = ZF +
    3.38    description {*
    3.39 @@ -174,7 +174,7 @@
    3.40  
    3.41      Comb            (*Combinatory Logic example*)
    3.42      Primrec         (*Primitive recursive functions*)
    3.43 -  files "document/root.tex"
    3.44 +  document_files "root.tex"
    3.45  
    3.46  session "ZF-Resid" in Resid = ZF +
    3.47    description {*