isabelle: src/HOL/ex/String.ML@b0139b83a5ee (annotated)

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	goal String.thy "hd(''ABCD'') = CHR ''A''";
2031 03a843f0f447 Ran expandshort paulson parents: 1266 diff changeset	2	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5	goal String.thy "hd(''ABCD'') ~= CHR ''B''";
2031 03a843f0f447 Ran expandshort paulson parents: 1266 diff changeset	6	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	goal String.thy "''ABCD'' ~= ''ABCX''";
2031 03a843f0f447 Ran expandshort paulson parents: 1266 diff changeset	10	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	goal String.thy "''ABCD'' = ''ABCD''";
2031 03a843f0f447 Ran expandshort paulson parents: 1266 diff changeset	14	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	goal String.thy
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	"''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
2031 03a843f0f447 Ran expandshort paulson parents: 1266 diff changeset	19	by (Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	result();

author	paulson
	Mon, 26 May 1997 12:33:03 +0200
changeset 3335	b0139b83a5ee
parent 2031	03a843f0f447
child 5069	3ea049f7979d
permissions	-rw-r--r--