clasohm@969: goal String.thy "hd(''ABCD'') = CHR ''A''";
paulson@2031: by (Simp_tac 1);
clasohm@969: result();
clasohm@969: 
clasohm@969: goal String.thy "hd(''ABCD'') ~= CHR ''B''";
paulson@2031: by (Simp_tac 1);
clasohm@969: result();
clasohm@969: 
clasohm@969: goal String.thy "''ABCD'' ~= ''ABCX''";
paulson@2031: by (Simp_tac 1);
clasohm@969: result();
clasohm@969: 
clasohm@969: goal String.thy "''ABCD'' = ''ABCD''";
paulson@2031: by (Simp_tac 1);
clasohm@969: result();
clasohm@969: 
clasohm@969: goal String.thy
clasohm@969:   "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
paulson@2031: by (Simp_tac 1);
clasohm@969: result();