src/HOL/Nat.thy
changeset 32772 50d090ca93f8
parent 32456 341c83339aeb
child 33274 b6ff7db522b5
     1.1 --- a/src/HOL/Nat.thy	Mon Sep 28 23:51:13 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Sep 30 08:21:53 2009 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    assumes "P 0"
     1.5      and "\<And>n. P n \<Longrightarrow> P (Suc n)"
     1.6    shows "P n"
     1.7 -  using assms by (rule nat.induct) 
     1.8 +  using assms by (rule nat.induct)
     1.9  
    1.10  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    1.11