src/HOL/Algebra/FiniteProduct.thy
changeset 35416 d8d7d1b785af
parent 35054 a5db9779b026
child 35847 19f1f7066917
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -26,8 +26,7 @@
     1.4  
     1.5  inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
     1.6  
     1.7 -constdefs
     1.8 -  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
     1.9 +definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
    1.10    "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
    1.11  
    1.12  lemma foldSetD_closed: