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/Number_Theory/Cong.thy
changeset 37293 2c9ed7478e6e
parent 36350 bc7982c54e37
child 41541 1fa4725c4656
equal deleted inserted replaced
37292:12a514e0319a 37293:2c9ed7478e6e 
    28 
    28 
    29 
    29 
    30 header {* Congruence *}
 
    30 header {* Congruence *}
 
    31 
    31 
    32 theory Cong
 
    32 theory Cong
 
    33 imports GCD Primes
 
    33 imports Primes
 
    34 begin
 
    34 begin
 
    35 
    35 
    36 subsection {* Turn off One_nat_def *}
 
    36 subsection {* Turn off One_nat_def *}
 
    37 
    37 
    38 lemma induct'_nat [case_names zero plus1, induct type: nat]: 
    38 lemma induct'_nat [case_names zero plus1, induct type: nat]:
isabelle