# HG changeset patch
# User wenzelm
# Date 1237295665 -3600
# Node ID e99c5466af9294a7d2cb819ff7b6934120505b1a
# Parent  7b0017587e7d6417a38fca58fa90fea8f144d307# Parent  0cc3b7f03ade4d757e79e3456d79ba4c3d7cde51
merged

diff -r 0cc3b7f03ade -r e99c5466af92 NEWS
--- a/NEWS	Tue Mar 17 14:12:43 2009 +0100
+++ b/NEWS	Tue Mar 17 14:14:25 2009 +0100
@@ -211,6 +211,25 @@
 
 *** HOL ***
 
+* Theory Library/Polynomial.thy defines an abstract type 'a poly of
+univariate polynomials with coefficients of type 'a.  In addition to
+the standard ring operations, it also supports div and mod.  Code
+generation is also supported, using list-style constructors.
+
+* Theory Library/Inner_Product.thy defines a class of real_inner for
+real inner product spaces, with an overloaded operation inner :: 'a =>
+'a => real.  Class real_inner is a subclass of real_normed_vector from
+RealVector.thy.
+
+* Theory Library/Product_Vector.thy provides instances for the product
+type 'a * 'b of several classes from RealVector.thy and
+Inner_Product.thy.  Definitions of addition, subtraction, scalar
+multiplication, norms, and inner products are included.
+
+* Theory Library/Bit.thy defines the field "bit" of integers modulo 2.
+In addition to the field operations, numerals and case syntax are also
+supported.
+
 * Theory Library/Diagonalize.thy provides constructive version of
 Cantor's first diagonalization argument.
 
@@ -241,7 +260,7 @@
 * Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order)
 now in directory HOL/Decision_Procs.
 
-* Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
+* Theory HOL/Decision_Procs/Approximation.thy provides the new proof method
 "approximation".  It proves formulas on real values by using interval arithmetic.
 In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
 exp and the constant pi are allowed. For examples see
diff -r 0cc3b7f03ade -r e99c5466af92 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Tue Mar 17 14:12:43 2009 +0100
+++ b/src/HOLCF/Universal.thy	Tue Mar 17 14:14:25 2009 +0100
@@ -159,20 +159,24 @@
 lemma ubasis_until_mono:
   assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b"
   shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)"
- apply (induct set: ubasis_le)
-    apply (rule ubasis_le_refl)
-   apply (erule (1) ubasis_le_trans)
-  apply (simp add: ubasis_le_refl)
-  apply (rule impI)
-  apply (rule ubasis_le_trans)
-   apply (rule ubasis_until_less)
-  apply (erule ubasis_le_lower)
- apply simp
- apply (rule impI)
- apply (subst ubasis_until_same)
-  apply (erule (3) prems)
- apply (erule (2) ubasis_le_upper)
-done
+proof (induct set: ubasis_le)
+  case (ubasis_le_refl a) show ?case by (rule ubasis_le.ubasis_le_refl)
+next
+  case (ubasis_le_trans a b c) thus ?case by - (rule ubasis_le.ubasis_le_trans)
+next
+  case (ubasis_le_lower S a i) thus ?case
+    apply (clarsimp simp add: ubasis_le_refl)
+    apply (rule ubasis_le_trans [OF ubasis_until_less])
+    apply (erule ubasis_le.ubasis_le_lower)
+    done
+next
+  case (ubasis_le_upper S b a i) thus ?case
+    apply clarsimp
+    apply (subst ubasis_until_same)
+     apply (erule (3) prems)
+    apply (erule (2) ubasis_le.ubasis_le_upper)
+    done
+qed
 
 lemma finite_range_ubasis_until:
   "finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))"
@@ -780,7 +784,7 @@
   case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
 next
   case (ubasis_le_lower S a i) thus ?case
-    apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+    apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
      apply (erule rangeE, rename_tac x)
      apply (simp add: basis_prj_basis_emb)
      apply (simp add: node_eq_basis_emb_iff)
@@ -790,7 +794,7 @@
     done
 next
   case (ubasis_le_upper S b a i) thus ?case
-    apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
+    apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
      apply (erule rangeE, rename_tac x)
      apply (simp add: basis_prj_basis_emb)
      apply (clarsimp simp add: node_eq_basis_emb_iff)