# HG changeset patch
# User huffman
# Date 1290961312 28800
# Node ID aeeb3e61e3af25b976216736820481190300b7de
# Parent  c52cd8bc426defc394569c625d1864f6b5d9c42d# Parent  d122dce6562d969bbe8bfd1e10918a9234f131d2
merged

diff -r c52cd8bc426d -r aeeb3e61e3af Admin/CHECKLIST
--- a/Admin/CHECKLIST	Sun Nov 28 07:29:32 2010 -0800
+++ b/Admin/CHECKLIST	Sun Nov 28 08:21:52 2010 -0800
@@ -1,9 +1,9 @@
 Checklist for official releases
 ===============================
 
-- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0, smlnj;
+- test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
 
-- test Proof General;
+- test Proof General 3.7.1.1, 4.0;
 
 - test Scala wrapper;
 
@@ -27,6 +27,7 @@
 
 - maintain Logics:
     build
+    etc/components
     lib/html/library_index_content.template
 
 
diff -r c52cd8bc426d -r aeeb3e61e3af Admin/makebin
--- a/Admin/makebin	Sun Nov 28 07:29:32 2010 -0800
+++ b/Admin/makebin	Sun Nov 28 08:21:52 2010 -0800
@@ -101,7 +101,7 @@
   ./build -bait
 else
   ./build -b -m HOL-Nominal HOL
-  ./build -b HOLCF
+  ./build -b -m HOLCF HOL
   ./build -b ZF
 fi
 
diff -r c52cd8bc426d -r aeeb3e61e3af NEWS
--- a/NEWS	Sun Nov 28 07:29:32 2010 -0800
+++ b/NEWS	Sun Nov 28 08:21:52 2010 -0800
@@ -683,7 +683,7 @@
 
 Tracing is then active for all invocations of the simplifier in
 subsequent goal refinement steps. Tracing may also still be enabled or
-disabled via the Proof General settings menu.
+disabled via the ProofGeneral settings menu.
 
 * Separate commands 'hide_class', 'hide_type', 'hide_const',
 'hide_fact' replace the former 'hide' KIND command.  Minor
diff -r c52cd8bc426d -r aeeb3e61e3af etc/components
--- a/etc/components	Sun Nov 28 07:29:32 2010 -0800
+++ b/etc/components	Sun Nov 28 08:21:52 2010 -0800
@@ -7,7 +7,6 @@
 src/CTT
 src/Cube
 src/FOLP
-src/HOLCF
 src/LCF
 src/Sequents
 #misc components
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -130,7 +130,7 @@
    apply (rule Suc_le_mono [THEN subst])
    apply (simp add: card_Suc_Diff1)
   apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
-     apply (blast intro: foldSetD_imp_finite finite_Diff)
+     apply (blast intro: foldSetD_imp_finite)
     apply best
    apply assumption
   apply (frule (1) Diff1_foldSetD)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Big_Operators.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -707,7 +707,7 @@
 proof -
   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
-    by(auto intro: finite_imageI)
+    by auto
   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Finite_Set.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -274,7 +274,7 @@
   then show ?thesis by simp
 qed
 
-lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
+lemma finite_Diff [simp, intro]: "finite A ==> finite (A - B)"
 by (rule Diff_subset [THEN finite_subset])
 
 lemma finite_Diff2 [simp]:
@@ -303,7 +303,7 @@
 
 text {* Image and Inverse Image over Finite Sets *}
 
-lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
+lemma finite_imageI[simp, intro]: "finite F ==> finite (h ` F)"
   -- {* The image of a finite set is finite. *}
   by (induct set: finite) simp_all
 
@@ -372,8 +372,9 @@
 
 text {* The finite UNION of finite sets *}
 
-lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
-  by (induct set: finite) simp_all
+lemma finite_UN_I[intro]:
+  "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
+by (induct set: finite) simp_all
 
 text {*
   Strengthen RHS to
@@ -385,7 +386,7 @@
 
 lemma finite_UN [simp]:
   "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
-by (blast intro: finite_UN_I finite_subset)
+by (blast intro: finite_subset)
 
 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
   finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
@@ -428,9 +429,9 @@
 
 text {* Sigma of finite sets *}
 
-lemma finite_SigmaI [simp]:
+lemma finite_SigmaI [simp, intro]:
     "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
-  by (unfold Sigma_def) (blast intro!: finite_UN_I)
+  by (unfold Sigma_def) blast
 
 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
     finite (A <*> B)"
@@ -2266,7 +2267,7 @@
 apply (induct set: finite)
  apply (simp_all add: Pow_insert)
 apply (subst card_Un_disjoint, blast)
-  apply (blast intro: finite_imageI, blast)
+  apply (blast, blast)
 apply (subgoal_tac "inj_on (insert x) (Pow F)")
  apply (simp add: card_image Pow_insert)
 apply (unfold inj_on_def)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/IMPP/Hoare.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -367,7 +367,7 @@
 apply  (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
 apply  (subgoal_tac "G = mgt_call ` U")
 prefer 2
-apply   (simp add: card_seteq finite_imageI)
+apply   (simp add: card_seteq)
 apply  simp
 apply  (erule prems(3-)) (*MGF_lemma1*)
 apply (rule ballI)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -339,7 +339,7 @@
   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
 proof (rule ccontr)
   assume "\<not> ?thesis"
-  with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
+  with img have "finite (UN y:f`A. f -` {y})" by blast
   moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
   moreover note dom
   ultimately show False by (simp add: infinite_super)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/List.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -3625,7 +3625,7 @@
   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
     by (auto simp:length_Suc_conv)
   then show ?case using `finite A`
-    by (auto intro: finite_imageI Suc) (* FIXME metis? *)
+    by (auto intro: Suc) (* FIXME metis? *)
 qed
 
 lemma finite_lists_length_le:
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -1300,7 +1300,7 @@
   shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
   and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
   unfolding  infnorm_set_image_cart
-  by (auto intro: finite_imageI)
+  by auto
 
 lemma component_le_infnorm_cart:
   shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -2929,7 +2929,7 @@
       using sf B(3)
       unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
       apply blast
-      using fB apply (blast intro: finite_imageI)
+      using fB apply blast
       unfolding d[symmetric]
       apply (rule card_image_le)
       apply (rule fB)
@@ -3035,7 +3035,7 @@
   shows "finite {abs((x::'a::euclidean_space)$$i) |i. i<DIM('a)}"
   and "{abs(x$$i) |i. i<DIM('a::euclidean_space)} \<noteq> {}"
   unfolding infnorm_set_image
-  by (auto intro: finite_imageI)
+  by auto
 
 lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
   unfolding infnorm_def
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -94,7 +94,7 @@
 subsection {* Properties of SetS *}
 
 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
-  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
+  by (auto simp add: SetS_def SRStar_finite [of p])
 
 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
   by (auto simp add: SetS_def MultInvPair_def)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -257,8 +257,7 @@
   apply (subst setprod_insert)
     apply (rule_tac [2] Bnor_prod_power_aux)
      apply (unfold inj_on_def)
-     apply (simp_all add: zmult_ac Bnor_fin finite_imageI
-       Bnor_mem_zle_swap)
+     apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap)
   done
 
 
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -55,7 +55,7 @@
 subsection {* Cardinality of explicit finite sets *}
 
 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
-  by (simp add: finite_subset finite_imageI)
+by (simp add: finite_subset)
 
 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
   by (rule bounded_nat_set_is_finite) blast
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -73,22 +73,22 @@
   done
 
 lemma finite_B: "finite (B)"
-  by (auto simp add: B_def finite_A finite_imageI)
+by (auto simp add: B_def finite_A)
 
 lemma finite_C: "finite (C)"
-  by (auto simp add: C_def finite_B finite_imageI)
+by (auto simp add: C_def finite_B)
 
 lemma finite_D: "finite (D)"
-  by (auto simp add: D_def finite_Int finite_C)
+by (auto simp add: D_def finite_Int finite_C)
 
 lemma finite_E: "finite (E)"
-  by (auto simp add: E_def finite_Int finite_C)
+by (auto simp add: E_def finite_Int finite_C)
 
 lemma finite_F: "finite (F)"
-  by (auto simp add: F_def finite_E finite_imageI)
+by (auto simp add: F_def finite_E)
 
 lemma C_eq: "C = D \<union> E"
-  by (auto simp add: C_def D_def E_def)
+by (auto simp add: C_def D_def E_def)
 
 lemma A_card_eq: "card A = nat ((p - 1) div 2)"
   apply (auto simp add: A_def)
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -511,7 +511,7 @@
       (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
       by auto
     hence "finite (?p ` (A \<inter> space M))"
-      by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }
+      by (rule finite_subset) auto }
   note this[intro, simp]
 
   { fix x assume "x \<in> space M"
diff -r c52cd8bc426d -r aeeb3e61e3af src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Sun Nov 28 07:29:32 2010 -0800
+++ b/src/HOL/ex/While_Combinator_Example.thy	Sun Nov 28 08:21:52 2010 -0800
@@ -28,7 +28,7 @@
  apply (fastsimp intro!: lfp_lowerbound)
  apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
 apply (clarsimp simp add: finite_psubset_def order_less_le)
-apply (blast intro!: finite_Diff dest: monoD)
+apply (blast dest: monoD)
 done