2013-06-27から1日間の記事一覧
定理自体はともかく,an_am_coprime の "0" の証明に even_zero_int 等を持ち出さないあたり,さすが metis といったところでしょう. theory prob01 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin fun a :: "nat => int" where "a 0 = 3" …
定理自体はともかく,an_am_coprime の "0" の証明に even_zero_int 等を持ち出さないあたり,さすが metis といったところでしょう. theory prob01 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin fun a :: "nat => int" where "a 0 = 3" …