# HG changeset patch
# User paulson
# Date 1107538474 -3600
# Node ID 3988e90613d4455de70feb0bc04662d2fa35eca9
# Parent  53bca254719adc8fcd32451c9e84af2cfb148fa2
comment

diff -r 53bca254719a -r 3988e90613d4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Feb 04 17:14:42 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Feb 04 18:34:34 2005 +0100
@@ -446,6 +446,13 @@
   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   "fold f g z A == THE x. (A, x) : foldSet f g z"
 
+text{*A tempting alternative for the definiens is
+@{term "if finite A then THE x. (A, x) : foldSet f g e else e"}.
+It allows the removal of finiteness assumptions from the theorems
+@{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
+The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
+
+
 lemma Diff1_foldSet:
   "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
 by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)