1.1 --- a/src/HOL/Int.thy	Tue Feb 17 20:45:23 2009 -0800
     1.2 +++ b/src/HOL/Int.thy	Wed Feb 18 10:26:48 2009 +0100
     1.3 @@ -1627,7 +1627,7 @@
     1.4  context ring_1
     1.5  begin
     1.6  
     1.7 -lemma of_int_of_nat:
     1.8 +lemma of_int_of_nat [nitpick_const_simp]:
     1.9    "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
    1.10  proof (cases "k < 0")
    1.11    case True then have "0 \<le> - k" by simp

     2.1 --- a/src/HOL/Tools/refute.ML	Tue Feb 17 20:45:23 2009 -0800
     2.2 +++ b/src/HOL/Tools/refute.ML	Wed Feb 18 10:26:48 2009 +0100
     2.3 @@ -2662,6 +2662,34 @@
     2.4    (* theory -> model -> arguments -> Term.term ->
     2.5      (interpretation * model * arguments) option *)
     2.6  
     2.7 +  fun set_interpreter thy model args t =
     2.8 +  let
     2.9 +    val (typs, terms) = model
    2.10 +  in
    2.11 +    case AList.lookup (op =) terms t of
    2.12 +      SOME intr =>
    2.13 +      (* return an existing interpretation *)
    2.14 +      SOME (intr, model, args)
    2.15 +    | NONE =>
    2.16 +      (case t of
    2.17 +      (* 'Collect' == identity *)
    2.18 +        Const (@{const_name Collect}, _) $ t1 =>
    2.19 +        SOME (interpret thy model args t1)
    2.20 +      | Const (@{const_name Collect}, _) =>
    2.21 +        SOME (interpret thy model args (eta_expand t 1))
    2.22 +      (* 'op :' == application *)
    2.23 +      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
    2.24 +        SOME (interpret thy model args (t2 $ t1))
    2.25 +      | Const (@{const_name "op :"}, _) $ t1 =>
    2.26 +        SOME (interpret thy model args (eta_expand t 1))
    2.27 +      | Const (@{const_name "op :"}, _) =>
    2.28 +        SOME (interpret thy model args (eta_expand t 2))
    2.29 +      | _ => NONE)
    2.30 +  end;
    2.31 +
    2.32 +  (* theory -> model -> arguments -> Term.term ->
    2.33 +    (interpretation * model * arguments) option *)
    2.34 +
    2.35    (* only an optimization: 'card' could in principle be interpreted with *)
    2.36    (* interpreters available already (using its definition), but the code *)
    2.37    (* below is more efficient                                             *)
    2.38 @@ -3271,6 +3299,7 @@
    2.39       add_interpreter "stlc"    stlc_interpreter #>
    2.40       add_interpreter "Pure"    Pure_interpreter #>
    2.41       add_interpreter "HOLogic" HOLogic_interpreter #>
    2.42 +     add_interpreter "set"     set_interpreter #>
    2.43       add_interpreter "IDT"             IDT_interpreter #>
    2.44       add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
    2.45       add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>