# HG changeset patch
# User urbanc
# Date 1297223548 0
# Node ID a3e0056c228bd8cb9b14704246f1b83085a0d989
# Parent  f41351709800d2be02e4cb745e41ddb2f0d5080c
separated the definition of folds into a separate file

diff -r f41351709800 -r a3e0056c228b Folds.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Folds.thy	Wed Feb 09 03:52:28 2011 +0000
@@ -0,0 +1,22 @@
+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