src/HOL/ex/StringEx.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5199 be986f7a6def
child 8035 84c5ce912b43
permissions -rw-r--r--
even more tidying of Goal commands
wenzelm@5199
     1
wenzelm@5199
     2
Goal "hd(''ABCD'') = CHR ''A''";
wenzelm@5199
     3
by (Simp_tac 1);
wenzelm@5199
     4
result();
wenzelm@5199
     5
wenzelm@5199
     6
Goal "hd(''ABCD'') ~= CHR ''B''";
wenzelm@5199
     7
by (Simp_tac 1);
wenzelm@5199
     8
result();
wenzelm@5199
     9
wenzelm@5199
    10
Goal "''ABCD'' ~= ''ABCX''";
wenzelm@5199
    11
by (Simp_tac 1);
wenzelm@5199
    12
result();
wenzelm@5199
    13
wenzelm@5199
    14
Goal "''ABCD'' = ''ABCD''";
wenzelm@5199
    15
by (Simp_tac 1);
wenzelm@5199
    16
result();
wenzelm@5199
    17
paulson@5278
    18
Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
wenzelm@5199
    19
by (Simp_tac 1);
wenzelm@5199
    20
result();