src/HOL/Nitpick.thy
changeset 67091 1393c2340eec
parent 67051 e7e54a0b9197
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Nitpick.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -150,10 +150,10 @@
     1.4    "one_frac \<equiv> Abs_Frac (1, 1)"
     1.5  
     1.6  definition num :: "'a \<Rightarrow> int" where
     1.7 -  "num \<equiv> fst o Rep_Frac"
     1.8 +  "num \<equiv> fst \<circ> Rep_Frac"
     1.9  
    1.10  definition denom :: "'a \<Rightarrow> int" where
    1.11 -  "denom \<equiv> snd o Rep_Frac"
    1.12 +  "denom \<equiv> snd \<circ> Rep_Frac"
    1.13  
    1.14  function norm_frac :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
    1.15    "norm_frac a b =