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/Integ/IntDef.thy
changeset 14269 502a7c95de73
parent 14259 79f7d3451b1e
child 14271 8ed6989228bb
equal deleted inserted replaced
14268:5cf13e80be0e 14269:502a7c95de73 
    36 
    36 
    37   (*For simplifying equalities*)
 
    37   (*For simplifying equalities*)
 
    38   iszero :: "int => bool"
 
    38   iszero :: "int => bool"
 
    39   "iszero z == z = (0::int)"
 
    39   "iszero z == z = (0::int)"
 
    40   
    40   
    41 defs (*of overloaded constants*)
 
    41 defs (overloaded)
 
    42   
    42   
    43   Zero_int_def:  "0 == int 0"
 
    43   Zero_int_def:  "0 == int 0"
 
    44   One_int_def:  "1 == int 1"
 
    44   One_int_def:  "1 == int 1"
 
    45 
    45 
    46   zadd_def:
 
    46   zadd_def:
isabelle