merged

--- a/src/HOL/Docs/MainDoc.thy	Fri Mar 06 22:50:30 2009 +0100
+++ b/src/HOL/Docs/MainDoc.thy	Fri Mar 06 23:25:08 2009 +0100
@@ -342,6 +342,36 @@
 \end{supertabular}
 
 
+\section{Set\_Interval}
+
+\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+@{const lessThan} & @{typeof lessThan}\\
+@{const atMost} & @{typeof atMost}\\
+@{const greaterThan} & @{typeof greaterThan}\\
+@{const atLeast} & @{typeof atLeast}\\
+@{const greaterThanLessThan} & @{typeof greaterThanLessThan}\\
+@{const atLeastLessThan} & @{typeof atLeastLessThan}\\
+@{const greaterThanAtMost} & @{typeof greaterThanAtMost}\\
+@{const atLeastAtMost} & @{typeof atLeastAtMost}\\
+\end{supertabular}
+
+\subsubsection*{Syntax}
+
+\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term "lessThan y"} & @{term[source] "lessThan y"}\\
+@{term "atMost y"} & @{term[source] "atMost y"}\\
+@{term "greaterThan x"} & @{term[source] "greaterThan x"}\\
+@{term "atLeast x"} & @{term[source] "atLeast x"}\\
+@{term "greaterThanLessThan x y"} & @{term[source] "greaterThanLessThan x y"}\\
+@{term "atLeastLessThan x y"} & @{term[source] "atLeastLessThan x y"}\\
+@{term "greaterThanAtMost x y"} & @{term[source] "greaterThanAtMost x y"}\\
+@{term "atLeastAtMost x y"} & @{term[source] "atLeastAtMost x y"}\\
+@{term "UN i:{..n}. A"} & @{term[source] "\<Union> i \<in> {..n}. A"}\\
+@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
+\end{supertabular}
+
+???????
+
 \section{Power}
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}

--- a/src/HOL/IntDiv.thy	Fri Mar 06 22:50:30 2009 +0100
+++ b/src/HOL/IntDiv.thy	Fri Mar 06 23:25:08 2009 +0100
@@ -1025,9 +1025,12 @@
 apply (auto simp add: div_eq_minus1)
 done
 
-lemma div_nonneg_neg_le0: "[| (0::int) \<le> a;  b < 0 |] ==> a div b \<le> 0"
+lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
 by (drule zdiv_mono1_neg, auto)
 
+lemma div_nonpos_pos_le0: "[| (a::int) \<le> 0; b > 0 |] ==> a div b \<le> 0"
+by (drule zdiv_mono1, auto)
+
 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)