--- a/Theories/Folds.thy	Tue May 31 20:32:49 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-theory Folds
-imports Main
-begin
-
-section {* Folds for Sets *}
-
-text {*
-  To obtain equational system out of finite set of equivalence classes, a fold operation
-  on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"}
-  more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"}
-  makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},
-  while @{text "fold f"} does not.  
-*}
-
-
-definition 
-  folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
-where
-  "folds f z S \<equiv> SOME x. fold_graph f z S x"
-
-
-end
\ No newline at end of file