src/HOL/Rat.thy
changeset 45183 2e1ad4a54189
parent 43889 90d24cafb05d
child 45478 8e299034eab4
     1.1 --- a/src/HOL/Rat.thy	Wed Oct 19 08:37:29 2011 +0200
     1.2 +++ b/src/HOL/Rat.thy	Wed Oct 19 09:11:14 2011 +0200
     1.3 @@ -1197,46 +1197,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -text {* Setup for SML code generator *}
     1.8 -
     1.9 -types_code
    1.10 -  rat ("(int */ int)")
    1.11 -attach (term_of) {*
    1.12 -fun term_of_rat (p, q) =
    1.13 -  let
    1.14 -    val rT = Type ("Rat.rat", [])
    1.15 -  in
    1.16 -    if q = 1 orelse p = 0 then HOLogic.mk_number rT p
    1.17 -    else @{term "op / \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"} $
    1.18 -      HOLogic.mk_number rT p $ HOLogic.mk_number rT q
    1.19 -  end;
    1.20 -*}
    1.21 -attach (test) {*
    1.22 -fun gen_rat i =
    1.23 -  let
    1.24 -    val p = random_range 0 i;
    1.25 -    val q = random_range 1 (i + 1);
    1.26 -    val g = Integer.gcd p q;
    1.27 -    val p' = p div g;
    1.28 -    val q' = q div g;
    1.29 -    val r = (if one_of [true, false] then p' else ~ p',
    1.30 -      if p' = 0 then 1 else q')
    1.31 -  in
    1.32 -    (r, fn () => term_of_rat r)
    1.33 -  end;
    1.34 -*}
    1.35 -
    1.36 -consts_code
    1.37 -  Fract ("(_,/ _)")
    1.38 -
    1.39 -consts_code
    1.40 -  quotient_of ("{*normalize*}")
    1.41 -
    1.42 -consts_code
    1.43 -  "of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
    1.44 -attach {*
    1.45 -fun rat_of_int i = (i, 1);
    1.46 -*}
    1.47 +subsection {* Setup for Nitpick *}
    1.48  
    1.49  declaration {*
    1.50    Nitpick_HOL.register_frac_type @{type_name rat}