| changeset 11583 | bebeb3b9e88e |
| parent 11582 | f666c1e4133d |
| child 11584 | c8e98b9498b4 |
| 11582:f666c1e4133d | 11583:bebeb3b9e88e |
|---|---|
1 |
|
2 Goal "hd(''ABCD'') = CHR ''A''"; |
|
3 by (Simp_tac 1); |
|
4 qed ""; |
|
5 |
|
6 Goal "hd(''ABCD'') ~= CHR ''B''"; |
|
7 by (Simp_tac 1); |
|
8 qed ""; |
|
9 |
|
10 Goal "''ABCD'' ~= ''ABCX''"; |
|
11 by (Simp_tac 1); |
|
12 qed ""; |
|
13 |
|
14 Goal "''ABCD'' = ''ABCD''"; |
|
15 by (Simp_tac 1); |
|
16 qed ""; |
|
17 |
|
18 Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; |
|
19 by (Simp_tac 1); |
|
20 qed ""; |