summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 20 Sep 2002 11:48:35 +0200 | |

changeset 13571 | d76a798281f4 |

parent 13570 | 0d6a0dce3ba3 |

child 13572 | 1681c5b58766 |

less use of x-symbols

--- a/src/HOL/Finite_Set.thy Thu Sep 19 16:09:16 2002 +0200 +++ b/src/HOL/Finite_Set.thy Fri Sep 20 11:48:35 2002 +0200 @@ -744,16 +744,16 @@ thus ?case by simp next case (insert F x) - have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))" + have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))" by simp - also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))" + also have "... = (f o g) x (fold (f o g) e (F \<union> B))" by (rule LC.fold_insert [OF LC.intro]) (insert b insert, auto simp add: left_commute) - also from insert have "fold (f \<circ> g) e (F \<union> B) = - fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast - also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B" + also from insert have "fold (f o g) e (F \<union> B) = + fold (f o g) e F \<cdot> fold (f o g) e B" by blast + also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B" by (simp add: AC) - also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)" + also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)" by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert, auto simp add: left_commute) finally show ?case .