Additional rules for inductive package.

--- a/src/HOL/equalities.ML	Tue Oct 05 15:25:35 1999 +0200
+++ b/src/HOL/equalities.ML	Tue Oct 05 15:25:52 1999 +0200
@@ -215,6 +215,9 @@
 by (Blast_tac 1);
 qed "Int_subset_iff";
 
+Goal "(x : A Int {x. P x}) = (x : A & P x)";
+by (Blast_tac 1);
+qed "Int_Collect";
 
 section "Un";
 

--- a/src/HOL/mono.ML	Tue Oct 05 15:25:35 1999 +0200
+++ b/src/HOL/mono.ML	Tue Oct 05 15:25:52 1999 +0200
@@ -115,3 +115,11 @@
 by (Force_tac 1);
 by (force_tac (claset() addSIs [order_antisym], simpset()) 1);
 qed "Least_mono";
+
+Goal "[| a = b; c = d; b --> d |] ==> a --> c";
+by (Fast_tac 1);
+qed "eq_to_mono";
+
+Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c";
+by (Fast_tac 1);
+qed "eq_to_mono2";