src/HOL/Library/Library.thy
changeset 66797 9c9baae29217
parent 66563 87b9eb69d5ba
child 67224 341fbce5b26d
     1.1 --- a/src/HOL/Library/Library.thy	Sun Oct 08 22:28:19 2017 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Sun Oct 08 22:28:19 2017 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    Countable_Set_Type
     1.5    Debug
     1.6    Diagonal_Subsequence
     1.7 +  Discrete
     1.8    Disjoint_Sets
     1.9    Dlist
    1.10    Extended
    1.11 @@ -28,7 +29,6 @@
    1.12    FSet
    1.13    FuncSet
    1.14    Function_Division
    1.15 -  Function_Growth
    1.16    Fun_Lexorder
    1.17    Going_To_Filter
    1.18    Groups_Big_Fun