src/HOL/Nitpick.thy
changeset 35028 108662d50512
parent 34982 7b8c366e34a2
child 35079 592edca1dfb3
     1.1 --- a/src/HOL/Nitpick.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -224,13 +224,13 @@
     1.4     "Nitpick_Nut" so that they handle the unexpanded overloaded constants
     1.5     directly, but this is slightly more tricky to implement. *)
     1.6  lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
     1.7 -    div_nat_inst.div_nat div_nat_inst.mod_nat lower_semilattice_fun_inst.inf_fun
     1.8 +    div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun
     1.9      minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
    1.10      one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
    1.11      ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
    1.12      ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
    1.13      times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
    1.14 -    upper_semilattice_fun_inst.sup_fun zero_int_inst.zero_int
    1.15 +    semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int
    1.16      zero_nat_inst.zero_nat
    1.17  
    1.18  use "Tools/Nitpick/kodkod.ML"