src/HOL/Library/Library.thy
changeset 38622 86fc906dcd86
parent 37818 dd65033fed78
child 40349 131cf8790a1c
--- a/src/HOL/Library/Library.thy	Fri Aug 20 17:46:56 2010 +0200
+++ b/src/HOL/Library/Library.thy	Fri Aug 20 17:48:30 2010 +0200
@@ -22,6 +22,7 @@
   FrechetDeriv
   Fset
   FuncSet
+  Function_Algebras
   Fundamental_Theorem_Algebra
   Indicator_Function
   Infinite_Set
@@ -54,6 +55,7 @@
   Ramsey
   Reflection
   RBT
+  Set_Algebras
   SML_Quickcheck
   State_Monad
   Sum_Of_Squares