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/Computational_Algebra/Primes.thy
changeset 66453 cc19f7ca2ed6
parent 65583 8d53b3bebab4
child 66837 6ba663ff2b1c
equal deleted inserted replaced
66452:450cefec7c11 66453:cc19f7ca2ed6 
    37 *)
 
    37 *)
 
    38 
    38 
    39 section \<open>Primes\<close>
 
    39 section \<open>Primes\<close>
 
    40 
    40 
    41 theory Primes
 
    41 theory Primes
 
    42 imports "~~/src/HOL/Binomial" Euclidean_Algorithm
 
    42 imports HOL.Binomial Euclidean_Algorithm
 
    43 begin
 
    43 begin
 
    44 
    44 
    45 (* As a simp or intro rule,
 
    45 (* As a simp or intro rule,
 
    46 
    46 
    47      prime p \<Longrightarrow> p > 0
 
    47      prime p \<Longrightarrow> p > 0
isabelle