changeset 7657 | dbbf7721126e |
parent 7561 | ff8dbd0589aa |
child 8229 | 38f453607c61 |
--- 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);