src/HOL/Number_Theory/Primes.thy
changeset 37765 26bdfb7b680b
parent 37607 ebb8b1a79c4c
child 40461 e876e95588ce
equal deleted inserted replaced
37764:3489daf839d5 37765:26bdfb7b680b
    43 begin
    43 begin
    44 
    44 
    45 definition
    45 definition
    46   prime_nat :: "nat \<Rightarrow> bool"
    46   prime_nat :: "nat \<Rightarrow> bool"
    47 where
    47 where
    48   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    48   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
    49 
    49 
    50 instance proof qed
    50 instance proof qed
    51 
    51 
    52 end
    52 end
    53 
    53 
    56 begin
    56 begin
    57 
    57 
    58 definition
    58 definition
    59   prime_int :: "int \<Rightarrow> bool"
    59   prime_int :: "int \<Rightarrow> bool"
    60 where
    60 where
    61   [code del]: "prime_int p = prime (nat p)"
    61   "prime_int p = prime (nat p)"
    62 
    62 
    63 instance proof qed
    63 instance proof qed
    64 
    64 
    65 end
    65 end
    66 
    66