# HG changeset patch
# User berghofe
# Date 939129952 -7200
# Node ID f4fe9d620107cf04e0bacabb02b294a3d5a87545
# Parent  c522ec2adc37cbc7f45fdb63d6013258c3f4256c
Additional rules for inductive package.

diff -r c522ec2adc37 -r f4fe9d620107 src/HOL/equalities.ML
--- 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";
 
diff -r c522ec2adc37 -r f4fe9d620107 src/HOL/mono.ML
--- 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";