[isabelle-dev] NEWS: Primes

2016-07-27 Thread Manuel Eberl
*** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" function, the "factorial_ring" typeclass with instance proofs for nat, int, poly. * Probability: Code generation and QuickCheck for Probability Mass Functio

Re: [isabelle-dev] NEWS: Primes

2016-07-27 Thread Tobias Nipkow
Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" function, the "factorial_ring" typeclass with instance proofs for nat, int, p

Re: [isabelle-dev] NEWS: Primes

2016-07-28 Thread Manuel Eberl
Yes, that might be a good idea. On 27/07/16 11:24, Tobias Nipkow wrote: Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" fun