src/HOL/Analysis/Linear_Algebra.thy
changeset 68607 67bb59e49834
parent 68224 1f7308050349
child 68901 4824cc40f42e
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -377,11 +377,11 @@
     1.4  subsection \<open>Archimedean properties and useful consequences\<close>
     1.5  
     1.6  text\<open>Bernoulli's inequality\<close>
     1.7 -proposition%important Bernoulli_inequality:
     1.8 +proposition Bernoulli_inequality:
     1.9    fixes x :: real
    1.10    assumes "-1 \<le> x"
    1.11      shows "1 + n * x \<le> (1 + x) ^ n"
    1.12 -proof%unimportant (induct n)
    1.13 +proof (induct n)
    1.14    case 0
    1.15    then show ?case by simp
    1.16  next