fixed quantifier handling of new monotonicity calculus
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 4100560d931de0709
parent 41004 01f33bf79596
child 41006 000ca46429cd
fixed quantifier handling of new monotonicity calculus
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -559,7 +559,7 @@
     1.4         |> map swap
     1.5         |> AList.group (op =)
     1.6         |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
     1.7 -                             string_for_vars ", " xs)
     1.8 +                             string_for_vars ", " (sort int_ord xs))
     1.9         |> space_implode "\n"))
    1.10  
    1.11  fun solve max_var (comps, clauses) =
    1.12 @@ -1044,7 +1044,7 @@
    1.13              fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
    1.14              val (body_m, accum) =
    1.15                accum ||> side_cond
    1.16 -                        ? add_mtype_is_complete [(x, (Minus, ann ()))] abs_M
    1.17 +                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
    1.18                      |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
    1.19              val body_M = mtype_of_mterm body_m
    1.20            in