# HG changeset patch
# User wenzelm
# Date 938616258 -7200
# Node ID dbbf7721126e6b3f9db8d8b0aca88846cde3dbb6
# Parent  2f18c0ffc348c11c18109a47771a2090d58a8eee
subsetD;

diff -r 2f18c0ffc348 -r dbbf7721126e src/HOL/Calculation.thy
--- a/src/HOL/Calculation.thy	Wed Sep 29 16:41:52 1999 +0200
+++ b/src/HOL/Calculation.thy	Wed Sep 29 16:44:18 1999 +0200
@@ -17,6 +17,12 @@
 
 theorems [trans] = dvd_trans;                               (* dvd dvd dvd *)
 
+theorem [trans]: "[| c:A; A <= B |] ==> c:B";
+  by (rule subsetD);
+
+theorem [trans]: "[| A <= B; c:A |] ==> c:B";
+  by (rule subsetD);
+
 theorem [trans]: "[| x ~= y; (x::'a::order) <= y |] ==> x < y";     (*  ~=  <=  < *)
   by (simp! add: order_less_le);