src/HOL/Library/Library.thy
changeset 63972 c98d1dd7eba1
parent 63971 da89140186e2
child 64588 293ab573d034
equal deleted inserted replaced
63971:da89140186e2 63972:c98d1dd7eba1
    59   Permutation
    59   Permutation
    60   Permutations
    60   Permutations
    61   Polynomial
    61   Polynomial
    62   Polynomial_FPS
    62   Polynomial_FPS
    63   Preorder
    63   Preorder
    64   Product_plus
    64   Product_Plus
    65   Quadratic_Discriminant
    65   Quadratic_Discriminant
    66   Quotient_List
    66   Quotient_List
    67   Quotient_Option
    67   Quotient_Option
    68   Quotient_Product
    68   Quotient_Product
    69   Quotient_Set
    69   Quotient_Set