# HG changeset patch # User huffman # Date 1266431436 28800 # Node ID 61255c81da010a8ffe1c785f8c5ba41cd9409f63 # Parent e15040ae75d7561cfb305a92f8494df98ebda2ec fix more looping simp rules diff -r e15040ae75d7 -r 61255c81da01 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 10:00:22 2010 -0800 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 17 10:30:36 2010 -0800 @@ -2864,8 +2864,8 @@ then have nz: "pochhammer (1 + b - of_nat n) n \ 0" by (auto simp add: algebra_simps) - from nz kn have nz': "pochhammer (1 + b - of_nat n) k \ 0" - by (simp add: pochhammer_neq_0_mono) + from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \ 0" + by (rule pochhammer_neq_0_mono) {assume k0: "k = 0 \ n =0" then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" using kn diff -r e15040ae75d7 -r 61255c81da01 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Wed Feb 17 10:00:22 2010 -0800 +++ b/src/HOL/Library/Ramsey.thy Wed Feb 17 10:30:36 2010 -0800 @@ -111,7 +111,7 @@ have infYx': "infinite (Yx-{yx'})" using fields px by auto with fields px yx' Suc.prems have partfx': "part r s (Yx - {yx'}) (f \ insert yx')" - by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY]) + by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx]) from Suc.hyps [OF infYx' partfx'] obtain Y' and t' where Y': "Y' \ Yx - {yx'}" "infinite Y'" "t' < s" diff -r e15040ae75d7 -r 61255c81da01 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Wed Feb 17 10:00:22 2010 -0800 +++ b/src/HOL/Library/Word.thy Wed Feb 17 10:30:36 2010 -0800 @@ -980,7 +980,8 @@ fix xs assume "length (norm_signed (\#xs)) = Suc (length xs)" thus "norm_signed (\#xs) = \#xs" - by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm) + by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI] + split: split_if_asm) next fix xs assume "length (norm_signed (\#xs)) = Suc (length xs)" diff -r e15040ae75d7 -r 61255c81da01 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Feb 17 10:00:22 2010 -0800 +++ b/src/HOL/Library/Zorn.thy Wed Feb 17 10:30:36 2010 -0800 @@ -333,7 +333,7 @@ lemma antisym_init_seg_of: "r initial_segment_of s \ s initial_segment_of r \ r=s" -by(auto simp:init_seg_of_def) +unfolding init_seg_of_def by safe lemma Chain_init_seg_of_Union: "R \ Chain init_seg_of \ r\R \ r initial_segment_of \R"