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

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	goal String.thy "hd(''ABCD'') = CHR ''A''";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 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''";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 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''";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 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''";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 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''";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 969 diff changeset	19	by(Simp_tac 1);
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	result();

author	paulson
	Thu, 18 Jan 1996 10:38:29 +0100
changeset 1444	23ceb1dc9755
parent 1266	3ae9fe3c0f68
child 2031	03a843f0f447
permissions	-rw-r--r--