src/HOL/ex/StringEx.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8035 84c5ce912b43
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     1
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     2
Goal "hd(''ABCD'') = CHR ''A''";
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     3
by (Simp_tac 1);
8035
84c5ce912b43 qed "";
wenzelm
parents: 5278
diff changeset
     4
qed "";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     5
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     6
Goal "hd(''ABCD'') ~= CHR ''B''";
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     7
by (Simp_tac 1);
8035
84c5ce912b43 qed "";
wenzelm
parents: 5278
diff changeset
     8
qed "";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     9
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    10
Goal "''ABCD'' ~= ''ABCX''";
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    11
by (Simp_tac 1);
8035
84c5ce912b43 qed "";
wenzelm
parents: 5278
diff changeset
    12
qed "";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    13
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    14
Goal "''ABCD'' = ''ABCD''";
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    15
by (Simp_tac 1);
8035
84c5ce912b43 qed "";
wenzelm
parents: 5278
diff changeset
    16
qed "";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    17
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5199
diff changeset
    18
Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    19
by (Simp_tac 1);
8035
84c5ce912b43 qed "";
wenzelm
parents: 5278
diff changeset
    20
qed "";