author | krauss |
Mon, 31 Jul 2006 18:05:40 +0200 | |
changeset 20269 | c40070317ab8 |
parent 20268 | 1fe9aed8fcac |
child 20270 | 3abe7dae681e |
--- a/src/HOL/Import/HOL4Compat.thy Mon Jul 31 15:29:36 2006 +0200 +++ b/src/HOL/Import/HOL4Compat.thy Mon Jul 31 18:05:40 2006 +0200 @@ -221,9 +221,7 @@ by simp lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))" - apply simp - apply arith - done + by simp lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)" by (simp add: max_def)