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

969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	1	val string_ss = list_ss addsimps (String.nibble.simps @ String.char.simps);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	goal String.thy "hd(''ABCD'') = CHR ''A''";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	by(simp_tac string_ss 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	goal String.thy "hd(''ABCD'') ~= CHR ''B''";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8	by(simp_tac string_ss 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11	goal String.thy "''ABCD'' ~= ''ABCX''";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	by(simp_tac string_ss 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15	goal String.thy "''ABCD'' = ''ABCD''";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16	by(simp_tac string_ss 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	result();
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19	goal String.thy
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	"''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	21	by(simp_tac string_ss 1);
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	result();

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 969	b051e2fc2e34
child 1266	3ae9fe3c0f68
permissions	-rw-r--r--