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/Lex/RegSet_of_nat_DA.ML
changeset 8741 61bc5ed22b62
parent 8442 96023903c2df
child 8777 0c1061ea7559
equal deleted inserted replaced
8740:fa6c4e4182d9 8741:61bc5ed22b62 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author:     Tobias Nipkow
 
     3     Author:     Tobias Nipkow
 
     4     Copyright   1998 TUM
 
     4     Copyright   1998 TUM
 
     5 *)
 
     5 *)
 
     6 
     6 
     7 Addsimps [in_set_butlast_appendI];
 
     7 Addsimps [in_set_butlast_appendI, less_SucI];
 
     8 AddIs    [in_set_butlast_appendI];
 
     8 AddIs    [in_set_butlast_appendI];
 
     9 Addsimps [image_eqI];
 
     9 Addsimps [image_eqI];
 
    10 
    10 
    11 (* Lists *)
 
    11 (* Lists *)
 
    12 
    12
isabelle