merged

--- a/NEWS	Tue May 11 21:27:09 2010 +0200
+++ b/NEWS	Tue May 11 17:20:11 2010 -0700
@@ -143,7 +143,11 @@
 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
 no longer shadowed.  INCOMPATIBILITY.
 
-* Dropped theorem duplicate comp_arith; use semiring_norm instead.  INCOMPATIBILITY.
+* Dropped theorem duplicate comp_arith; use semiring_norm instead.
+INCOMPATIBILITY.
+
+* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
+INCOMPATIBILITY.
 
 * Theory 'Finite_Set': various folding_* locales facilitate the application
 of the various fold combinators on finite sets.

--- a/src/HOL/RealPow.thy	Tue May 11 21:27:09 2010 +0200
+++ b/src/HOL/RealPow.thy	Tue May 11 17:20:11 2010 -0700
@@ -88,17 +88,4 @@
 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
 by (auto simp add: power2_eq_square)
 
-(* The following theorem is by Benjamin Porter *)
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma real_sq_order:
-  fixes x :: "'a::linordered_semidom"
-  assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
-  shows "x \<le> y"
-proof -
-  from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
-    by (simp only: numeral_2_eq_2)
-  thus "x \<le> y" using ygt0
-    by (rule power_le_imp_le_base)
-qed
-
 end

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue May 11 21:27:09 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue May 11 17:20:11 2010 -0700
@@ -154,7 +154,7 @@
 val retraction_strict = @{thm retraction_strict};
 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
+val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
 
 (* ----- theorems concerning one induction step ----------------------------- *)
 
@@ -287,22 +287,17 @@
           map (K(atac 1)) (filter is_rec args))
         cons))
       conss);
-  local 
-    (* check whether every/exists constructor of the n-th part of the equation:
-       it has a possibly indirectly recursive argument that isn't/is possibly 
-       indirectly lazy *)
-    fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
+  local
+    fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg => 
           is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
-          ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
-            rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
+          ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
+            rec_of arg <> n andalso rec_to (rec_of arg::ns) 
               (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
           ) o snd) cons;
-    fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
     fun warn (n,cons) =
-      if all_rec_to [] false (n,cons)
+      if rec_to [] false (n,cons)
       then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
       else false;
-    fun lazy_rec_to ns = rec_to exists I  lazy_rec_to ns;
 
   in
     val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;