author | paulson |
Thu, 25 Jun 1998 13:57:34 +0200 | |
changeset 5078 | 7b5ea59c0275 |
parent 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
5069 | 1 |
Goal "hd(''ABCD'') = CHR ''A''"; |
2031 | 2 |
by (Simp_tac 1); |
969 | 3 |
result(); |
4 |
||
5069 | 5 |
Goal "hd(''ABCD'') ~= CHR ''B''"; |
2031 | 6 |
by (Simp_tac 1); |
969 | 7 |
result(); |
8 |
||
5069 | 9 |
Goal "''ABCD'' ~= ''ABCX''"; |
2031 | 10 |
by (Simp_tac 1); |
969 | 11 |
result(); |
12 |
||
5069 | 13 |
Goal "''ABCD'' = ''ABCD''"; |
2031 | 14 |
by (Simp_tac 1); |
969 | 15 |
result(); |
16 |
||
5069 | 17 |
Goal |
969 | 18 |
"''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; |
2031 | 19 |
by (Simp_tac 1); |
969 | 20 |
result(); |