src/HOL/Library/Library.thy

--- a/src/HOL/Library/Library.thy	Thu Apr 06 08:33:37 2017 +0200
+++ b/src/HOL/Library/Library.thy	Thu Apr 06 21:37:13 2017 +0200
@@ -25,13 +25,10 @@
   Extended_Real
   Finite_Map
   Float
-  Formal_Power_Series
-  Fraction_Field
   FSet
   FuncSet
   Function_Division
   Function_Growth
-  Fundamental_Theorem_Algebra
   Fun_Lexorder
   Groups_Big_Fun
   Indicator_Function
@@ -59,8 +56,6 @@
   Perm
   Permutation
   Permutations
-  Polynomial
-  Polynomial_FPS
   Preorder
   Product_Plus
   Quadratic_Discriminant