src/HOL/Main.thy
changeset 12554 671b4d632c34
parent 12439 e90a4f5a27f0
child 13093 ab0335307905
equal deleted inserted replaced
12553:90ac72455fcc 12554:671b4d632c34
   114   "snd"     ("snd")
   114   "snd"     ("snd")
   115 
   115 
   116   "Nil"     ("[]")
   116   "Nil"     ("[]")
   117   "Cons"    ("(_ ::/ _)")
   117   "Cons"    ("(_ ::/ _)")
   118 
   118 
       
   119 lemma [code]: "((n::nat) < 0) = False" by simp
       
   120 declare less_Suc_eq [code]
       
   121 
   119 end
   122 end