equal
deleted
inserted
replaced
564 |
564 |
565 |
565 |
566 subsection {* A basic fold functional for finite sets *} |
566 subsection {* A basic fold functional for finite sets *} |
567 |
567 |
568 text {* The intended behaviour is |
568 text {* The intended behaviour is |
569 @{text "fold f z {x\<^isub>1, ..., x\<^isub>n} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} |
569 @{text "fold f z {x\<^sub>1, ..., x\<^sub>n} = f x\<^sub>1 (\<dots> (f x\<^sub>n z)\<dots>)"} |
570 if @{text f} is ``left-commutative'': |
570 if @{text f} is ``left-commutative'': |
571 *} |
571 *} |
572 |
572 |
573 locale comp_fun_commute = |
573 locale comp_fun_commute = |
574 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
574 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |