src/HOL/ROOT
changeset 65678 aaba2e0c247c
parent 65576 8376f83f9094
child 65956 639eb3617a86
equal deleted inserted replaced
65677:7d25b8dbdbfa 65678:aaba2e0c247c
    69 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
    69 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
    70   theories
    70   theories
    71     Approximations
    71     Approximations
    72     Circle_Area
    72     Circle_Area
    73 
    73 
    74 session "HOL-Computational_Algebra" in "Computational_Algebra" = "HOL-Library" +
    74 session "HOL-Computational_Algebra" (timing) in "Computational_Algebra" = "HOL-Library" +
    75   theories
    75   theories
    76     Computational_Algebra
    76     Computational_Algebra
    77     (*conflicting type class instantiations and dependent applications*)
    77     (*conflicting type class instantiations and dependent applications*)
    78     Field_as_Ring
    78     Field_as_Ring
    79     Polynomial_Factorial
    79     Polynomial_Factorial
   560     Basic theory of lattices and orders.
   560     Basic theory of lattices and orders.
   561   *}
   561   *}
   562   theories CompleteLattice
   562   theories CompleteLattice
   563   document_files "root.tex"
   563   document_files "root.tex"
   564 
   564 
   565 session "HOL-ex" in ex = "HOL-Library" +
   565 session "HOL-ex" (timing) in ex = "HOL-Library" +
   566   description {*
   566   description {*
   567     Miscellaneous examples for Higher-Order Logic.
   567     Miscellaneous examples for Higher-Order Logic.
   568   *}
   568   *}
   569   options [document = false]
   569   options [document = false]
   570   sessions
   570   sessions