# HG changeset patch
# User huffman
# Date 1266509331 28800
# Node ID b9866ad4e3be229a5744394c9221f38d62fee961
# Parent  3979b07298028e01118b260fe94c7884855489d9
fix looping call to simplifier

diff -r 3979b0729802 -r b9866ad4e3be src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Feb 17 22:32:05 2010 +0100
+++ b/src/HOL/Transcendental.thy	Thu Feb 18 08:08:51 2010 -0800
@@ -247,7 +247,7 @@
         from f[OF this]
         show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
       next
-        case False hence "even (n - 1)" using even_num_iff odd_pos by auto 
+        case False hence "even (n - 1)" by simp
         from even_nat_div_two_times_two[OF this]
         have n_eq: "2 * ((n - 1) div 2) = n - 1" unfolding numeral_2_eq_2[symmetric] by auto
         hence range_eq: "n - 1 + 1 = n" using odd_pos[OF False] by auto