src/HOL/Main.thy
changeset 12554 671b4d632c34
parent 12439 e90a4f5a27f0
child 13093 ab0335307905
     1.1 --- a/src/HOL/Main.thy	Wed Dec 19 13:21:12 2001 +0100
     1.2 +++ b/src/HOL/Main.thy	Thu Dec 20 14:55:28 2001 +0100
     1.3 @@ -116,4 +116,7 @@
     1.4    "Nil"     ("[]")
     1.5    "Cons"    ("(_ ::/ _)")
     1.6  
     1.7 +lemma [code]: "((n::nat) < 0) = False" by simp
     1.8 +declare less_Suc_eq [code]
     1.9 +
    1.10  end