equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
7 Addsimps [in_set_butlast_appendI]; |
8 AddIs [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
8 AddIs [in_set_butlast_appendI]; |
9 Addsimps [image_eqI]; |
9 Addsimps [image_eqI]; |
10 |
10 |
11 (* Lists *) |
11 (* Lists *) |
12 |
12 |
13 Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"; |
13 Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"; |