# 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);