src/HOL/NumberTheory/IntPrimes.thy
changeset 10147 178deaacb244
parent 9943 55c82decf3f4
child 11049 7eef34adb852
equal deleted inserted replaced
10146:e89309dde9d3 10147:178deaacb244
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:	Thomas M. Rasmussen
     3     Author:	Thomas M. Rasmussen
     4     Copyright	2000  University of Cambridge
     4     Copyright	2000  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 IntPrimes = Main + IntDiv + Primes +
     7 IntPrimes = Primes +
     8 
     8 
     9 consts
     9 consts
    10   xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
    10   xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
    11   xzgcd    :: "[int,int] => int*int*int" 
    11   xzgcd    :: "[int,int] => int*int*int" 
    12   zprime   :: int set
    12   zprime   :: int set