src/HOL/String.ML
author wenzelm
Fri, 03 Jul 1998 17:33:47 +0200
changeset 5121 5c1f89ae8aef
permissions -rw-r--r--
moved String theory to main HOL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     1
Goal "hd(''ABCD'') = CHR ''A''";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     2
by (Simp_tac 1);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     3
result();
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     4
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     5
Goal "hd(''ABCD'') ~= CHR ''B''";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     6
by (Simp_tac 1);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     7
result();
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     8
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     9
Goal "''ABCD'' ~= ''ABCX''";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    10
by (Simp_tac 1);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    11
result();
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    12
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    13
Goal "''ABCD'' = ''ABCD''";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    14
by (Simp_tac 1);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    15
result();
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    16
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    17
Goal
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    18
  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    19
by (Simp_tac 1);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    20
result();