author | nipkow |
Tue, 14 Oct 2008 13:24:07 +0200 | |
changeset 28584 | 58ac551ce1ce |
parent 28583 | 9bb9791bdc18 |
child 28585 | be3c44ac3e86 |
--- a/src/HOL/ex/Fundefs.thy Tue Oct 14 13:23:31 2008 +0200 +++ b/src/HOL/ex/Fundefs.thy Tue Oct 14 13:24:07 2008 +0200 @@ -87,7 +87,9 @@ with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp qed - +text{* Now trivial (even though it does not belong here): *} +lemma "f91 n = (if 100 < n then n - 10 else 91)" +by (induct n rule:f91.induct) auto subsection {* More general patterns *}