src/HOL/ROOT
changeset 64591 240a39af9ec4
parent 64588 293ab573d034
child 64597 1c252d8b6ca6
equal deleted inserted replaced
64590:6621d91d3c8a 64591:240a39af9ec4
    29   description {*
    29   description {*
    30     Classical Higher-order Logic -- batteries included.
    30     Classical Higher-order Logic -- batteries included.
    31   *}
    31   *}
    32   theories
    32   theories
    33     Library
    33     Library
    34     Polynomial_Factorial
       
    35     (*conflicting type class instantiations and dependent applications*)
    34     (*conflicting type class instantiations and dependent applications*)
       
    35     Field_as_Ring
    36     Finite_Lattice
    36     Finite_Lattice
    37     List_lexord
    37     List_lexord
       
    38     Polynomial_Factorial
    38     Prefix_Order
    39     Prefix_Order
    39     Product_Lexorder
    40     Product_Lexorder
    40     Product_Order
    41     Product_Order
    41     Sublist_Order
    42     Sublist_Order
    42     (*data refinements and dependent applications*)
    43     (*data refinements and dependent applications*)