| changeset 7028 | 6ea3b385e731 |
| parent 6831 | 799859f2e657 |
| child 7032 | d6efb3b8e669 |
| 7027:ca0fbe679bbb | 7028:6ea3b385e731 |
|---|---|
85 by (induct_tac "xs" 1); |
85 by (induct_tac "xs" 1); |
86 by Auto_tac; |
86 by Auto_tac; |
87 qed "length_rev"; |
87 qed "length_rev"; |
88 Addsimps [length_rev]; |
88 Addsimps [length_rev]; |
89 |
89 |
90 Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1"; |
90 Goal "length(tl xs) = (length xs) - 1"; |
91 by (exhaust_tac "xs" 1); |
91 by (exhaust_tac "xs" 1); |
92 by Auto_tac; |
92 by Auto_tac; |
93 qed "length_tl"; |
93 qed "length_tl"; |
94 Addsimps [length_tl]; |
94 Addsimps [length_tl]; |
95 |
95 |