isabelle: src/HOL/ex/StringEx.ML@e653cb933293 (annotated)

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 "";

author	nipkow
	Tue, 17 Oct 2000 08:00:46 +0200
changeset 10228	e653cb933293
parent 8035	84c5ce912b43
permissions	-rw-r--r--