src/HOL/Nitpick.thy
changeset 67051 e7e54a0b9197
parent 66011 f10bbfe07c41
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Nitpick.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Nitpick.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -137,7 +137,7 @@
     1.4    by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
     1.5  
     1.6  definition Frac :: "int \<times> int \<Rightarrow> bool" where
     1.7 -  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
     1.8 +  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b"
     1.9  
    1.10  consts
    1.11    Abs_Frac :: "int \<times> int \<Rightarrow> 'a"