1.1 --- a/Admin/CHECKLIST Sun Nov 28 07:29:32 2010 -0800
1.2 +++ b/Admin/CHECKLIST Sun Nov 28 08:21:52 2010 -0800
1.3 @@ -1,9 +1,9 @@
1.4 Checklist for official releases
1.5 ===============================
1.6
1.7 -- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0, smlnj;
1.8 +- test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
1.9
1.10 -- test Proof General;
1.11 +- test Proof General 3.7.1.1, 4.0;
1.12
1.13 - test Scala wrapper;
1.14
1.15 @@ -27,6 +27,7 @@
1.16
1.17 - maintain Logics:
1.18 build
1.19 + etc/components
1.20 lib/html/library_index_content.template
1.21
1.22
2.1 --- a/Admin/makebin Sun Nov 28 07:29:32 2010 -0800
2.2 +++ b/Admin/makebin Sun Nov 28 08:21:52 2010 -0800
2.3 @@ -101,7 +101,7 @@
2.4 ./build -bait
2.5 else
2.6 ./build -b -m HOL-Nominal HOL
2.7 - ./build -b HOLCF
2.8 + ./build -b -m HOLCF HOL
2.9 ./build -b ZF
2.10 fi
2.11
3.1 --- a/NEWS Sun Nov 28 07:29:32 2010 -0800
3.2 +++ b/NEWS Sun Nov 28 08:21:52 2010 -0800
3.3 @@ -683,7 +683,7 @@
3.4
3.5 Tracing is then active for all invocations of the simplifier in
3.6 subsequent goal refinement steps. Tracing may also still be enabled or
3.7 -disabled via the Proof General settings menu.
3.8 +disabled via the ProofGeneral settings menu.
3.9
3.10 * Separate commands 'hide_class', 'hide_type', 'hide_const',
3.11 'hide_fact' replace the former 'hide' KIND command. Minor
4.1 --- a/etc/components Sun Nov 28 07:29:32 2010 -0800
4.2 +++ b/etc/components Sun Nov 28 08:21:52 2010 -0800
4.3 @@ -7,7 +7,6 @@
4.4 src/CTT
4.5 src/Cube
4.6 src/FOLP
4.7 -src/HOLCF
4.8 src/LCF
4.9 src/Sequents
4.10 #misc components
5.1 --- a/src/HOL/Algebra/FiniteProduct.thy Sun Nov 28 07:29:32 2010 -0800
5.2 +++ b/src/HOL/Algebra/FiniteProduct.thy Sun Nov 28 08:21:52 2010 -0800
5.3 @@ -130,7 +130,7 @@
5.4 apply (rule Suc_le_mono [THEN subst])
5.5 apply (simp add: card_Suc_Diff1)
5.6 apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
5.7 - apply (blast intro: foldSetD_imp_finite finite_Diff)
5.8 + apply (blast intro: foldSetD_imp_finite)
5.9 apply best
5.10 apply assumption
5.11 apply (frule (1) Diff1_foldSetD)
6.1 --- a/src/HOL/Big_Operators.thy Sun Nov 28 07:29:32 2010 -0800
6.2 +++ b/src/HOL/Big_Operators.thy Sun Nov 28 08:21:52 2010 -0800
6.3 @@ -707,7 +707,7 @@
6.4 proof -
6.5 have "A <+> B = Inl ` A \<union> Inr ` B" by auto
6.6 moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
6.7 - by(auto intro: finite_imageI)
6.8 + by auto
6.9 moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
6.10 moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
6.11 ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)
7.1 --- a/src/HOL/Finite_Set.thy Sun Nov 28 07:29:32 2010 -0800
7.2 +++ b/src/HOL/Finite_Set.thy Sun Nov 28 08:21:52 2010 -0800
7.3 @@ -274,7 +274,7 @@
7.4 then show ?thesis by simp
7.5 qed
7.6
7.7 -lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
7.8 +lemma finite_Diff [simp, intro]: "finite A ==> finite (A - B)"
7.9 by (rule Diff_subset [THEN finite_subset])
7.10
7.11 lemma finite_Diff2 [simp]:
7.12 @@ -303,7 +303,7 @@
7.13
7.14 text {* Image and Inverse Image over Finite Sets *}
7.15
7.16 -lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
7.17 +lemma finite_imageI[simp, intro]: "finite F ==> finite (h ` F)"
7.18 -- {* The image of a finite set is finite. *}
7.19 by (induct set: finite) simp_all
7.20
7.21 @@ -372,8 +372,9 @@
7.22
7.23 text {* The finite UNION of finite sets *}
7.24
7.25 -lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
7.26 - by (induct set: finite) simp_all
7.27 +lemma finite_UN_I[intro]:
7.28 + "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
7.29 +by (induct set: finite) simp_all
7.30
7.31 text {*
7.32 Strengthen RHS to
7.33 @@ -385,7 +386,7 @@
7.34
7.35 lemma finite_UN [simp]:
7.36 "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
7.37 -by (blast intro: finite_UN_I finite_subset)
7.38 +by (blast intro: finite_subset)
7.39
7.40 lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
7.41 finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
7.42 @@ -428,9 +429,9 @@
7.43
7.44 text {* Sigma of finite sets *}
7.45
7.46 -lemma finite_SigmaI [simp]:
7.47 +lemma finite_SigmaI [simp, intro]:
7.48 "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
7.49 - by (unfold Sigma_def) (blast intro!: finite_UN_I)
7.50 + by (unfold Sigma_def) blast
7.51
7.52 lemma finite_cartesian_product: "[| finite A; finite B |] ==>
7.53 finite (A <*> B)"
7.54 @@ -2266,7 +2267,7 @@
7.55 apply (induct set: finite)
7.56 apply (simp_all add: Pow_insert)
7.57 apply (subst card_Un_disjoint, blast)
7.58 - apply (blast intro: finite_imageI, blast)
7.59 + apply (blast, blast)
7.60 apply (subgoal_tac "inj_on (insert x) (Pow F)")
7.61 apply (simp add: card_image Pow_insert)
7.62 apply (unfold inj_on_def)
8.1 --- a/src/HOL/IMPP/Hoare.thy Sun Nov 28 07:29:32 2010 -0800
8.2 +++ b/src/HOL/IMPP/Hoare.thy Sun Nov 28 08:21:52 2010 -0800
8.3 @@ -367,7 +367,7 @@
8.4 apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
8.5 apply (subgoal_tac "G = mgt_call ` U")
8.6 prefer 2
8.7 -apply (simp add: card_seteq finite_imageI)
8.8 +apply (simp add: card_seteq)
8.9 apply simp
8.10 apply (erule prems(3-)) (*MGF_lemma1*)
8.11 apply (rule ballI)
9.1 --- a/src/HOL/Library/Infinite_Set.thy Sun Nov 28 07:29:32 2010 -0800
9.2 +++ b/src/HOL/Library/Infinite_Set.thy Sun Nov 28 08:21:52 2010 -0800
9.3 @@ -339,7 +339,7 @@
9.4 shows "\<exists>y \<in> f`A. infinite (f -` {y})"
9.5 proof (rule ccontr)
9.6 assume "\<not> ?thesis"
9.7 - with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
9.8 + with img have "finite (UN y:f`A. f -` {y})" by blast
9.9 moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
9.10 moreover note dom
9.11 ultimately show False by (simp add: infinite_super)
10.1 --- a/src/HOL/List.thy Sun Nov 28 07:29:32 2010 -0800
10.2 +++ b/src/HOL/List.thy Sun Nov 28 08:21:52 2010 -0800
10.3 @@ -3625,7 +3625,7 @@
10.4 have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
10.5 by (auto simp:length_Suc_conv)
10.6 then show ?case using `finite A`
10.7 - by (auto intro: finite_imageI Suc) (* FIXME metis? *)
10.8 + by (auto intro: Suc) (* FIXME metis? *)
10.9 qed
10.10
10.11 lemma finite_lists_length_le:
11.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 28 07:29:32 2010 -0800
11.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Nov 28 08:21:52 2010 -0800
11.3 @@ -1300,7 +1300,7 @@
11.4 shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
11.5 and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
11.6 unfolding infnorm_set_image_cart
11.7 - by (auto intro: finite_imageI)
11.8 + by auto
11.9
11.10 lemma component_le_infnorm_cart:
11.11 shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
12.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Nov 28 07:29:32 2010 -0800
12.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Nov 28 08:21:52 2010 -0800
12.3 @@ -2929,7 +2929,7 @@
12.4 using sf B(3)
12.5 unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
12.6 apply blast
12.7 - using fB apply (blast intro: finite_imageI)
12.8 + using fB apply blast
12.9 unfolding d[symmetric]
12.10 apply (rule card_image_le)
12.11 apply (rule fB)
12.12 @@ -3035,7 +3035,7 @@
12.13 shows "finite {abs((x::'a::euclidean_space)$$i) |i. i<DIM('a)}"
12.14 and "{abs(x$$i) |i. i<DIM('a::euclidean_space)} \<noteq> {}"
12.15 unfolding infnorm_set_image
12.16 - by (auto intro: finite_imageI)
12.17 + by auto
12.18
12.19 lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
12.20 unfolding infnorm_def
13.1 --- a/src/HOL/Old_Number_Theory/Euler.thy Sun Nov 28 07:29:32 2010 -0800
13.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy Sun Nov 28 08:21:52 2010 -0800
13.3 @@ -94,7 +94,7 @@
13.4 subsection {* Properties of SetS *}
13.5
13.6 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
13.7 - by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
13.8 + by (auto simp add: SetS_def SRStar_finite [of p])
13.9
13.10 lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
13.11 by (auto simp add: SetS_def MultInvPair_def)
14.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy Sun Nov 28 07:29:32 2010 -0800
14.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sun Nov 28 08:21:52 2010 -0800
14.3 @@ -257,8 +257,7 @@
14.4 apply (subst setprod_insert)
14.5 apply (rule_tac [2] Bnor_prod_power_aux)
14.6 apply (unfold inj_on_def)
14.7 - apply (simp_all add: zmult_ac Bnor_fin finite_imageI
14.8 - Bnor_mem_zle_swap)
14.9 + apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap)
14.10 done
14.11
14.12
15.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy Sun Nov 28 07:29:32 2010 -0800
15.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy Sun Nov 28 08:21:52 2010 -0800
15.3 @@ -55,7 +55,7 @@
15.4 subsection {* Cardinality of explicit finite sets *}
15.5
15.6 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
15.7 - by (simp add: finite_subset finite_imageI)
15.8 +by (simp add: finite_subset)
15.9
15.10 lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
15.11 by (rule bounded_nat_set_is_finite) blast
16.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy Sun Nov 28 07:29:32 2010 -0800
16.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Sun Nov 28 08:21:52 2010 -0800
16.3 @@ -73,22 +73,22 @@
16.4 done
16.5
16.6 lemma finite_B: "finite (B)"
16.7 - by (auto simp add: B_def finite_A finite_imageI)
16.8 +by (auto simp add: B_def finite_A)
16.9
16.10 lemma finite_C: "finite (C)"
16.11 - by (auto simp add: C_def finite_B finite_imageI)
16.12 +by (auto simp add: C_def finite_B)
16.13
16.14 lemma finite_D: "finite (D)"
16.15 - by (auto simp add: D_def finite_Int finite_C)
16.16 +by (auto simp add: D_def finite_Int finite_C)
16.17
16.18 lemma finite_E: "finite (E)"
16.19 - by (auto simp add: E_def finite_Int finite_C)
16.20 +by (auto simp add: E_def finite_Int finite_C)
16.21
16.22 lemma finite_F: "finite (F)"
16.23 - by (auto simp add: F_def finite_E finite_imageI)
16.24 +by (auto simp add: F_def finite_E)
16.25
16.26 lemma C_eq: "C = D \<union> E"
16.27 - by (auto simp add: C_def D_def E_def)
16.28 +by (auto simp add: C_def D_def E_def)
16.29
16.30 lemma A_card_eq: "card A = nat ((p - 1) div 2)"
16.31 apply (auto simp add: A_def)
17.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy Sun Nov 28 07:29:32 2010 -0800
17.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Sun Nov 28 08:21:52 2010 -0800
17.3 @@ -511,7 +511,7 @@
17.4 (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
17.5 by auto
17.6 hence "finite (?p ` (A \<inter> space M))"
17.7 - by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }
17.8 + by (rule finite_subset) auto }
17.9 note this[intro, simp]
17.10
17.11 { fix x assume "x \<in> space M"
18.1 --- a/src/HOL/ex/While_Combinator_Example.thy Sun Nov 28 07:29:32 2010 -0800
18.2 +++ b/src/HOL/ex/While_Combinator_Example.thy Sun Nov 28 08:21:52 2010 -0800
18.3 @@ -28,7 +28,7 @@
18.4 apply (fastsimp intro!: lfp_lowerbound)
18.5 apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
18.6 apply (clarsimp simp add: finite_psubset_def order_less_le)
18.7 -apply (blast intro!: finite_Diff dest: monoD)
18.8 +apply (blast dest: monoD)
18.9 done
18.10
18.11