# HG changeset patch
# User paulson
# Date 837090881 -7200
# Node ID bec272e3e888cdcaa95b52b4f7779e740ff2f6be
# Parent  e251196383cdc48e436f9f5552a31a2d555340fb
Added insert_mono

diff -r e251196383cd -r bec272e3e888 src/HOL/mono.ML
--- a/src/HOL/mono.ML	Thu Jul 11 15:13:52 1996 +0200
+++ b/src/HOL/mono.ML	Thu Jul 11 15:14:41 1996 +0200
@@ -45,6 +45,10 @@
 by (fast_tac (!claset addIs [prem RS subsetD]) 1);
 qed "INT1_mono";
 
+goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D";
+by (Fast_tac 1);
+qed "insert_mono";
+
 goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
 by (Fast_tac 1);
 qed "Un_mono";