src/HOL/Finite_Set.thy
equal inserted replaced
`   705   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)`
`   705   also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc)`
`   706   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)`
`   706   also have "z \<cdot> x = x \<cdot> z" by (simp only: commute)`
`   707   finally show ?thesis .`
`   707   finally show ?thesis .`
`   708 qed`
`   708 qed`
`   709 `
`   709 `
`   710 lemma (in ACe)`
`   710 lemmas (in ACe) AC = assoc commute left_commute`
`   711     AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"  "x \<cdot> y = y \<cdot> x"  "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"`
`       `
`   712   by (rule assoc, rule commute, rule left_commute)  (* FIXME localize "lemmas" (!??) *)`
`       `
`   713 `
`   711 `
`   714 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"`
`   712 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x"`
`   715 proof -`
`   713 proof -`
`   716   have "x \<cdot> e = x" by (rule ident)`
`   714   have "x \<cdot> e = x" by (rule ident)`
`   717   thus ?thesis by (subst commute)`
`   715   thus ?thesis by (subst commute)`