| changeset 26649 | a053f13bc9da |
| parent 19738 | 1ac610922636 |
| child 35174 | e15040ae75d7 |
| 26648:25c07f3878b0 | 26649:a053f13bc9da |
|---|---|
37 by blast |
37 by blast |
38 |
38 |
39 |
39 |
40 subsection {* Lists *} |
40 subsection {* Lists *} |
41 |
41 |
42 lemma hd_append: "hd(l@m) = (if l~=[] then hd(l) else hd(m))" |
|
43 by (induct l) simp_all |
|
44 |
|
45 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))" |
42 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))" |
46 by (induct l) simp_all |
43 by (induct l) simp_all |
47 |
44 |
48 end |
45 end |