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/Transfer_Int_Nat.thy
changeset 67118 ccab07d1196c
parent 66954 0230af0f3c59
child 67399 eab6ce8368fa
equal deleted inserted replaced
67117:19f627407264 67118:ccab07d1196c 
    84 lemma ZN_numeral [transfer_rule]:
 
    84 lemma ZN_numeral [transfer_rule]:
 
    85   "(op = ===> ZN) numeral numeral"
 
    85   "(op = ===> ZN) numeral numeral"
 
    86   unfolding rel_fun_def ZN_def by simp
 
    86   unfolding rel_fun_def ZN_def by simp
 
    87 
    87 
    88 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
 
    88 lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
 
    89   unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
 
    89   unfolding rel_fun_def ZN_def by simp
 
    90 
    90 
    91 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
 
    91 lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
 
    92   unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
 
    92   unfolding rel_fun_def ZN_def by (simp add: zdiv_int)
 
    93 
    93 
    94 lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
 
    94 lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
isabelle