isabelle: src/HOL/ex/String.ML@aa5ea943f8e3 (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, 27 Apr 1998 13:47:46 +0200
changeset 4829	aa5ea943f8e3
parent 2031	03a843f0f447
child 5069	3ea049f7979d
permissions	-rw-r--r--