src/HOL/ROOT
changeset 51421 b5d559b101d9
parent 51403 2ff3a5589b05
child 51422 821a70e29e0b
     1.1 --- a/src/HOL/ROOT	Wed Mar 13 17:06:45 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Wed Mar 13 17:13:22 2013 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4  chapter HOL
     1.5  
     1.6  session HOL (main) = Pure +
     1.7 -  description {* Classical Higher-order Logic *}
     1.8 +  description {*
     1.9 +    Classical Higher-order Logic.
    1.10 +  *}
    1.11    options [document_graph]
    1.12    theories Complex_Main
    1.13    files
    1.14 @@ -11,7 +13,9 @@
    1.15      "document/root.tex"
    1.16  
    1.17  session "HOL-Proofs" = Pure +
    1.18 -  description {* HOL-Main with explicit proof terms *}
    1.19 +  description {*
    1.20 +    HOL-Main with explicit proof terms.
    1.21 +  *}
    1.22    options [document = false, proofs = 2]
    1.23    theories Main
    1.24    files
    1.25 @@ -19,7 +23,9 @@
    1.26      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    1.27  
    1.28  session "HOL-Library" (main) in Library = HOL +
    1.29 -  description {* Classical Higher-order Logic -- batteries included *}
    1.30 +  description {*
    1.31 +    Classical Higher-order Logic -- batteries included.
    1.32 +  *}
    1.33    theories
    1.34      Library
    1.35      (*conflicting type class instantiations*)
    1.36 @@ -264,7 +270,9 @@
    1.37    files "document/root.bib" "document/root.tex"
    1.38  
    1.39  session "HOL-Auth" in Auth = HOL +
    1.40 -  description {* A new approach to verifying authentication protocols. *}
    1.41 +  description {*
    1.42 +    A new approach to verifying authentication protocols.
    1.43 +  *}
    1.44    options [document_graph]
    1.45    theories
    1.46      Auth_Shared
    1.47 @@ -346,7 +354,9 @@
    1.48    theories Hilbert_Classical
    1.49  
    1.50  session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
    1.51 -  description {* Examples for program extraction in Higher-Order Logic *}
    1.52 +  description {*
    1.53 +    Examples for program extraction in Higher-Order Logic.
    1.54 +  *}
    1.55    options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
    1.56    theories [document = false]
    1.57      "~~/src/HOL/Library/Code_Target_Numeral"
    1.58 @@ -471,7 +481,9 @@
    1.59    files "document/root.tex"
    1.60  
    1.61  session "HOL-ex" in ex = HOL +
    1.62 -  description {* Miscellaneous examples for Higher-Order Logic. *}
    1.63 +  description {*
    1.64 +    Miscellaneous examples for Higher-Order Logic.
    1.65 +  *}
    1.66    options [timeout = 3600, condition = ISABELLE_POLYML]
    1.67    theories [document = false]
    1.68      "~~/src/HOL/Library/State_Monad"
    1.69 @@ -669,12 +681,16 @@
    1.70    theories [quick_and_dirty] VC_Condition
    1.71  
    1.72  session "HOL-Cardinals-Base" in Cardinals = HOL +
    1.73 -  description {* Ordinals and Cardinals, Base Theories *}
    1.74 +  description {*
    1.75 +    Ordinals and Cardinals, Base Theories.
    1.76 +  *}
    1.77    options [document = false]
    1.78    theories Cardinal_Arithmetic
    1.79  
    1.80  session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
    1.81 -  description {* Ordinals and Cardinals, Full Theories *}
    1.82 +  description {*
    1.83 +    Ordinals and Cardinals, Full Theories.
    1.84 +  *}
    1.85    options [document = false]
    1.86    theories Cardinals
    1.87    files
    1.88 @@ -683,17 +699,23 @@
    1.89      "document/root.bib"
    1.90  
    1.91  session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
    1.92 -  description {* Bounded Natural Functors for Datatypes *}
    1.93 +  description {*
    1.94 +    Bounded Natural Functors for Datatypes.
    1.95 +  *}
    1.96    options [document = false]
    1.97    theories BNF_LFP
    1.98  
    1.99  session "HOL-BNF" in BNF = "HOL-Cardinals" +
   1.100 -  description {* Bounded Natural Functors for (Co)datatypes *}
   1.101 +  description {*
   1.102 +    Bounded Natural Functors for (Co)datatypes.
   1.103 +  *}
   1.104    options [document = false]
   1.105    theories BNF
   1.106  
   1.107  session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
   1.108 -  description {* Examples for Bounded Natural Functors *}
   1.109 +  description {*
   1.110 +    Examples for Bounded Natural Functors.
   1.111 +  *}
   1.112    options [document = false]
   1.113    theories
   1.114      Lambda_Term
   1.115 @@ -720,7 +742,9 @@
   1.116    files "document/root.tex"
   1.117  
   1.118  session "HOL-NSA" in NSA = HOL +
   1.119 -  description {* Nonstandard analysis. *}
   1.120 +  description {*
   1.121 +    Nonstandard analysis.
   1.122 +  *}
   1.123    options [document_graph]
   1.124    theories Hypercomplex
   1.125    files "document/root.tex"
   1.126 @@ -958,7 +982,9 @@
   1.127    files "document/root.tex"
   1.128  
   1.129  session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   1.130 -  description {* Misc HOLCF examples *}
   1.131 +  description {*
   1.132 +    Miscellaneous examples for HOLCF.
   1.133 +  *}
   1.134    options [document = false]
   1.135    theories
   1.136      Dnat
   1.137 @@ -1046,7 +1072,9 @@
   1.138      TrivEx2
   1.139  
   1.140  session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   1.141 -  description {* Some rather large datatype examples (from John Harrison). *}
   1.142 +  description {*
   1.143 +    Some rather large datatype examples (from John Harrison).
   1.144 +  *}
   1.145    options [document = false]
   1.146    theories [condition = ISABELLE_FULL_TEST, timing]
   1.147      Brackin
   1.148 @@ -1055,7 +1083,9 @@
   1.149      Verilog
   1.150  
   1.151  session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   1.152 -  description {* Some benchmark on large record. *}
   1.153 +  description {*
   1.154 +    Some benchmark on large record.
   1.155 +  *}
   1.156    options [document = false]
   1.157    theories [condition = ISABELLE_FULL_TEST, timing]
   1.158      Record_Benchmark