Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/StringEx.ML
changeset 8035 84c5ce912b43
parent 5278 a903b66822e2
equal deleted inserted replaced
8034:6fc37b5c5e98 8035:84c5ce912b43 
     1 
     1 
     2 Goal "hd(''ABCD'') = CHR ''A''";
 
     2 Goal "hd(''ABCD'') = CHR ''A''";
 
     3 by (Simp_tac 1);
 
     3 by (Simp_tac 1);
 
     4 result();
 
     4 qed "";
 
     5 
     5 
     6 Goal "hd(''ABCD'') ~= CHR ''B''";
 
     6 Goal "hd(''ABCD'') ~= CHR ''B''";
 
     7 by (Simp_tac 1);
 
     7 by (Simp_tac 1);
 
     8 result();
 
     8 qed "";
 
     9 
     9 
    10 Goal "''ABCD'' ~= ''ABCX''";
 
    10 Goal "''ABCD'' ~= ''ABCX''";
 
    11 by (Simp_tac 1);
 
    11 by (Simp_tac 1);
 
    12 result();
 
    12 qed "";
 
    13 
    13 
    14 Goal "''ABCD'' = ''ABCD''";
 
    14 Goal "''ABCD'' = ''ABCD''";
 
    15 by (Simp_tac 1);
 
    15 by (Simp_tac 1);
 
    16 result();
 
    16 qed "";
 
    17 
    17 
    18 Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
 
    18 Goal "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''";
 
    19 by (Simp_tac 1);
 
    19 by (Simp_tac 1);
 
    20 result();
 
    20 qed "";
isabelle