diff -r 408713c7f66b -r deec279dda0a ex/String.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/String.ML Fri Feb 03 16:19:45 1995 +0100 @@ -0,0 +1,22 @@ +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();