author | clasohm |
Fri, 01 Dec 1995 12:03:13 +0100 | |
changeset 1376 | 92f83b9d17e1 |
parent 1266 | 3ae9fe3c0f68 |
child 2031 | 03a843f0f447 |
permissions | -rw-r--r-- |
969 | 1 |
goal String.thy "hd(''ABCD'') = CHR ''A''"; |
1266 | 2 |
by(Simp_tac 1); |
969 | 3 |
result(); |
4 |
||
5 |
goal String.thy "hd(''ABCD'') ~= CHR ''B''"; |
|
1266 | 6 |
by(Simp_tac 1); |
969 | 7 |
result(); |
8 |
||
9 |
goal String.thy "''ABCD'' ~= ''ABCX''"; |
|
1266 | 10 |
by(Simp_tac 1); |
969 | 11 |
result(); |
12 |
||
13 |
goal String.thy "''ABCD'' = ''ABCD''"; |
|
1266 | 14 |
by(Simp_tac 1); |
969 | 15 |
result(); |
16 |
||
17 |
goal String.thy |
|
18 |
"''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; |
|
1266 | 19 |
by(Simp_tac 1); |
969 | 20 |
result(); |