src/HOL/Library/Library.thy
changeset 73477 1d8a79aa2a99
parent 73326 7a88313895d5
child 73622 4dc3baf45d6a
--- a/src/HOL/Library/Library.thy	Wed Mar 24 21:17:19 2021 +0100
+++ b/src/HOL/Library/Library.thy	Thu Mar 25 08:52:15 2021 +0000
@@ -51,13 +51,11 @@
   Lattice_Constructions
   Linear_Temporal_Logic_on_Streams
   ListVector
-  List_Permutation
   Lub_Glb
   Mapping
   Monad_Syntax
   More_List
   Multiset_Order
-  Multiset_Permutations
   Nonpos_Ints
   Numeral_Type
   Omega_Words_Fun
@@ -68,7 +66,6 @@
   Pattern_Aliases
   Periodic_Fun
   Perm
-  Permutations
   Poly_Mapping
   Power_By_Squaring
   Preorder
@@ -89,7 +86,6 @@
   Set_Idioms
   Signed_Division
   State_Monad
-  Stirling
   Stream
   Sorting_Algorithms
   Sublist