src/HOL/Library/Library.thy
changeset 31849 431d8588bcad
parent 31807 039893a9a77d
child 31990 1d4d0b305f16
--- a/src/HOL/Library/Library.thy	Mon Jun 29 12:18:54 2009 +0200
+++ b/src/HOL/Library/Library.thy	Mon Jun 29 12:18:55 2009 +0200
@@ -10,7 +10,6 @@
   Char_ord
   Code_Char_chr
   Code_Integer
-  Code_Set
   Coinductive_List
   Commutative_Ring
   Continuity
@@ -28,6 +27,7 @@
   Formal_Power_Series
   Fraction_Field
   FrechetDeriv
+  Fset
   FuncSet
   Fundamental_Theorem_Algebra
   Infinite_Set