Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
changeset 35416 d8d7d1b785af
parent 35267 8dfd816713c6
child 35577 43b93e294522 
--- a/src/HOL/Finite_Set.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -2528,8 +2528,7 @@
   fold1Set_insertI [intro]:
    "\<lbrakk> fold_graph f a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
 
-constdefs
-  fold1 :: "('a => 'a => 'a) => 'a set => 'a"
+definition fold1 :: "('a => 'a => 'a) => 'a set => 'a" where
   "fold1 f A == THE x. fold1Set f A x"
 
 lemma fold1Set_nonempty:
isabelle