src/HOL/ex/String.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 2031 03a843f0f447
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
clasohm@969
     1
goal String.thy "hd(''ABCD'') = CHR ''A''";
paulson@2031
     2
by (Simp_tac 1);
clasohm@969
     3
result();
clasohm@969
     4
clasohm@969
     5
goal String.thy "hd(''ABCD'') ~= CHR ''B''";
paulson@2031
     6
by (Simp_tac 1);
clasohm@969
     7
result();
clasohm@969
     8
clasohm@969
     9
goal String.thy "''ABCD'' ~= ''ABCX''";
paulson@2031
    10
by (Simp_tac 1);
clasohm@969
    11
result();
clasohm@969
    12
clasohm@969
    13
goal String.thy "''ABCD'' = ''ABCD''";
paulson@2031
    14
by (Simp_tac 1);
clasohm@969
    15
result();
clasohm@969
    16
clasohm@969
    17
goal String.thy
clasohm@969
    18
  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
paulson@2031
    19
by (Simp_tac 1);
clasohm@969
    20
result();