| changeset 5121 | 5c1f89ae8aef |
| 5120:f7f5442c934a | 5121:5c1f89ae8aef |
|---|---|
1 Goal "hd(''ABCD'') = CHR ''A''"; |
|
2 by (Simp_tac 1); |
|
3 result(); |
|
4 |
|
5 Goal "hd(''ABCD'') ~= CHR ''B''"; |
|
6 by (Simp_tac 1); |
|
7 result(); |
|
8 |
|
9 Goal "''ABCD'' ~= ''ABCX''"; |
|
10 by (Simp_tac 1); |
|
11 result(); |
|
12 |
|
13 Goal "''ABCD'' = ''ABCD''"; |
|
14 by (Simp_tac 1); |
|
15 result(); |
|
16 |
|
17 Goal |
|
18 "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; |
|
19 by (Simp_tac 1); |
|
20 result(); |