src/HOL/Nitpick.thy
changeset 35220 2bcdae5f4fdb
parent 35180 c57dba973391
child 35284 9edc2bd6d2bd
     1.1 --- a/src/HOL/Nitpick.thy	Thu Feb 18 10:38:37 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Thu Feb 18 18:48:07 2010 +0100
     1.3 @@ -217,21 +217,6 @@
     1.4  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
     1.5  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
     1.6  
     1.7 -(* While Nitpick normally avoids to unfold definitions for locales, it
     1.8 -   unfortunately needs to unfold them when dealing with the following built-in
     1.9 -   constants. A cleaner approach would be to change "Nitpick_HOL" and
    1.10 -   "Nitpick_Nut" so that they handle the unexpanded overloaded constants
    1.11 -   directly, but this is slightly more tricky to implement. *)
    1.12 -lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
    1.13 -    div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun
    1.14 -    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
    1.15 -    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
    1.16 -    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
    1.17 -    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
    1.18 -    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
    1.19 -    semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int
    1.20 -    zero_nat_inst.zero_nat
    1.21 -
    1.22  use "Tools/Nitpick/kodkod.ML"
    1.23  use "Tools/Nitpick/kodkod_sat.ML"
    1.24  use "Tools/Nitpick/nitpick_util.ML"