src/HOL/ex/String.ML

New theory and proofs including preorder, inorder, ..., initially
from ZF/ex/BT. Demonstrates datatypes and primrec.

val string_ss = list_ss addsimps (String.nibble.simps @ String.char.simps);

goal String.thy "hd(''ABCD'') = CHR ''A''";
by(simp_tac string_ss 1);
result();

goal String.thy "hd(''ABCD'') ~= CHR ''B''";
by(simp_tac string_ss 1);
result();

goal String.thy "''ABCD'' ~= ''ABCX''";
by(simp_tac string_ss 1);
result();

goal String.thy "''ABCD'' = ''ABCD''";
by(simp_tac string_ss 1);
result();

goal String.thy
  "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
by(simp_tac string_ss 1);
result();