# HG changeset patch
# User paulson
# Date 864644080 -7200
# Node ID 3f9a806f061eeab57e9f75eb974a88e79625f58a
# Parent  4e7dfe8ae41baa4fbcc7c9c2cef828a9743adeaf
Two useful facts about Powersets suggested by Florian Kammueller

diff -r 4e7dfe8ae41b -r 3f9a806f061e src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon May 26 12:53:45 1997 +0200
+++ b/src/HOL/equalities.ML	Mon May 26 12:54:40 1997 +0200
@@ -605,6 +605,18 @@
 by (Blast_tac 1);
 qed "subset_iff_psubset_eq";
 
+goalw Set.thy [Pow_def] "Pow {} = {{}}";
+by (Auto_tac());
+qed "Pow_empty";
+Addsimps [Pow_empty];
+
+goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
+by (Step_tac 1);
+be swap 1;
+by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
+by (ALLGOALS Blast_tac);
+qed "Pow_insert";
+
 
 (** Miniscoping: pushing in big Unions and Intersections **)
 local