src/HOL/ROOT

     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
   document_files
     "root.bib"
     "root.tex"
 
-session "HOL-Proofs" = Pure +
+session "HOL-Proofs" (timing) = Pure +
   description {*
     HOL-Main with explicit proof terms.
   *}
   options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)

   theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
-session "HOL-Library" (main) in Library = HOL +
+session "HOL-Library" (main timing) in Library = HOL +
   description {*
     Classical Higher-order Logic -- batteries included.
   *}
   theories
     Library

     Comb
     PropLog
     Com
   document_files "root.tex"
 
-session "HOL-IMP" in IMP = HOL +
+session "HOL-IMP" (timing) in IMP = HOL +
   options [document_variants = document]
   theories [document = false]
     "~~/src/HOL/Library/While_Combinator"
     "~~/src/HOL/Library/Char_ord"
     "~~/src/HOL/Library/List_lexord"

     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   *}
   options [document = false]
   theories EvenOdd
 
-session "HOL-Data_Structures" in Data_Structures = HOL +
+session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   theories [document = false]
     "Less_False"
     "~~/src/HOL/Library/Multiset"
     "~~/src/HOL/Library/Float"

 
 session "HOL-Import" in Import = HOL +
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
-session "HOL-Number_Theory" in Number_Theory = HOL +
+session "HOL-Number_Theory" (timing) in Number_Theory = HOL +
   description {*
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   *}
   theories [document = false]

     automatically from pre/post conditions and loop invariants).
   *}
   theories Hoare
   document_files "root.bib" "root.tex"
 
-session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
+session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
   description {*
     Verification of shared-variable imperative programs a la Owicki-Gries.
     (verification conditions are generated automatically).
   *}
   theories Hoare_Parallel

   theories [condition = "ISABELLE_SCALA"]
     Code_Test_Scala
   theories [condition = "ISABELLE_SMLNJ"]
     Code_Test_SMLNJ
 
-session "HOL-Metis_Examples" in Metis_Examples = HOL +
+session "HOL-Metis_Examples" (timing) in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.

     Copyright   2009
   *}
   options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
-session "HOL-Algebra" (main) in Algebra = HOL +
+session "HOL-Algebra" (main timing) in Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
     The Isabelle Algebraic Library.
   *}

     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
   document_files "root.bib" "root.tex"
 
-session "HOL-Auth" in Auth = HOL +
+session "HOL-Auth" (timing) in Auth = HOL +
   description {*
     A new approach to verifying authentication protocols.
   *}
   theories
     Auth_Shared

     "Smartcard/Auth_Smartcard"
     "Guard/Auth_Guard_Shared"
     "Guard/Auth_Guard_Public"
   document_files "root.tex"
 
-session "HOL-UNITY" in UNITY = "HOL-Auth" +
+session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     Verifying security protocols using Chandy and Misra's UNITY formalism.

     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Library/LaTeXsugar"
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
-session "HOL-Decision_Procs" in Decision_Procs = HOL +
+session "HOL-Decision_Procs" (timing) in Decision_Procs = HOL +
   description {*
     Various decision procedures, typically involving reflection.
   *}
   options [document = false]
   theories Decision_Procs

   theories
     Hilbert_Classical
     Proof_Terms
     XML_Data
 
-session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
+session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
   options [parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]

     Higman_Extraction
     Pigeonhole
     Euclid
   document_files "root.bib" "root.tex"
 
-session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
+session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   description {*
     Lambda Calculus in de Bruijn's Notation.
 
     This session defines lambda-calculus terms with de Bruijn indixes and
     proves confluence of beta, eta and beta+eta.

     a little functional language and its type system.
   *}
   options [document = false]
   theories Test Type
 
-session "HOL-MicroJava" in MicroJava = HOL +
+session "HOL-MicroJava" (timing) in MicroJava = HOL +
   description {*
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   *}

     Hoare Logic for a tiny fragment of Java.
   *}
   theories Example
   document_files "root.bib" "root.tex"
 
-session "HOL-Bali" in Bali = HOL +
+session "HOL-Bali" (timing) in Bali = HOL +
   theories
     AxExample
     AxSound
     AxCompl
     Trans

     Eisbach
     Tests
     Examples
     Examples_FOL
 
-session "HOL-SET_Protocol" in SET_Protocol = HOL +
+session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   description {*
     Verification of the SET Protocol.
   *}
   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   theories SET_Protocol

     THF_Arith
     TPTP_Proof_Reconstruction
   theories
     ATP_Problem_Import
 
-session "HOL-Analysis" (main) in Analysis = HOL +
+session "HOL-Analysis" (main timing) in Analysis = HOL +
   theories
     Analysis
   document_files
     "root.tex"
 
 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
   theories
     Approximations
 
-session "HOL-Probability" in "Probability" = "HOL-Analysis" +
+session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Permutation"
     "~~/src/HOL/Library/Order_Continuity"
     "~~/src/HOL/Library/Diagonal_Subsequence"
     "~~/src/HOL/Library/Finite_Map"
   theories
     Probability
   document_files "root.tex"
 
-session "HOL-Probability-ex" in "Probability/ex" = "HOL-Probability" +
+session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   theories
     "Dining_Cryptographers"
     "Koepf_Duermuth_Countermeasure"
     "Measure_Not_CCC"
 
 session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
   theories Nominal
 
-session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
+session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   options [document = false]
   theories
     Class3
     CK_Machine
     Compile

     Weakening
     W
   theories [quick_and_dirty]
     VC_Condition
 
-session "HOL-Cardinals" in Cardinals = HOL +
+session "HOL-Cardinals" (timing) in Cardinals = HOL +
   description {*
     Ordinals and Cardinals, Full Theories.
   *}
   options [document = false]
   theories

   document_files
     "intro.tex"
     "root.tex"
     "root.bib"
 
-session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
+session "HOL-Datatype_Examples" (timing) in Datatype_Examples = HOL +
   description {*
     (Co)datatype Examples.
   *}
   options [document = false]
   theories

     Misc_Codatatype
     Misc_Datatype
     Misc_Primcorec
     Misc_Primrec
 
-session "HOL-Corec_Examples" in Corec_Examples = HOL +
+session "HOL-Corec_Examples" (timing) in Corec_Examples = HOL +
   description {*
     Corecursion Examples.
   *}
   options [document = false]
   theories

     "Tests/Small_Concrete"
     "Tests/Stream_Friends"
     "Tests/TLList_Friends"
     "Tests/Type_Class"
 
-session "HOL-Word" (main) in Word = HOL +
+session "HOL-Word" (main timing) in Word = HOL +
   theories Word
   document_files "root.bib" "root.tex"
 
 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   options [document = false]

 session "HOL-Statespace" in Statespace = HOL +
   theories [skip_proofs = false]
     StateSpaceEx
   document_files "root.tex"
 
-session "HOL-Nonstandard_Analysis" in Nonstandard_Analysis = HOL +
+session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = HOL +
   description {*
     Nonstandard analysis.
   *}
   theories
     Nonstandard_Analysis
   document_files "root.tex"
 
-session "HOL-Nonstandard_Analysis-Examples" in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
+session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   options [document = false]
   theories NSPrimes
 
 session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]

 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   options [document = false, timeout = 60]
   theories Ex
 
-session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
+session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]
   theories
     Boogie
     SMT_Examples
     SMT_Word_Examples

 
 session "HOL-Mutabelle" in Mutabelle = HOL +
   options [document = false]
   theories MutabelleExtra
 
-session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
   options [document = false]
   theories
     Quickcheck_Examples
     Quickcheck_Lattice_Examples
     Completeness

     Quickcheck_Nesting_Example
   theories [condition = ISABELLE_GHC]
     Hotel_Example
     Quickcheck_Narrowing_Examples
 
-session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" (timing) in Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
   options [document = false]
   theories

     Quotient_Rat
     Lift_DList
     Int_Pow
     Lifting_Code_Dt_Test
 
-session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
   options [document = false]
   theories
     Examples
     Predicate_Compile_Tests
     Predicate_Compile_Quickcheck_Examples

     Lambda_Example
     List_Examples
   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
     Reg_Exp_Example
 
-session HOLCF (main) in HOLCF = HOL +
+session HOLCF (main timing) in HOLCF = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.

   theories
     Fstreams
     FOCUS
     Buffer_adm
 
-session IOA in "HOLCF/IOA" = HOLCF +
+session IOA (timing) in "HOLCF/IOA" = HOLCF +
   description {*
     Author:     Olaf Mueller
     Copyright   1997 TU München
 
     A formalization of I/O automata in HOLCF.