--- a/src/HOL/Finite_Set.thy Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Finite_Set.thy Fri Aug 17 13:58:57 2007 +0200
@@ -2424,7 +2424,6 @@
have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
using insert
- thm ACIf.fold1_insert_idem_def
by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"