src/HOL/Tools/Qelim/cooper.ML
changeset 28397 389c5e494605
parent 28290 4cc2b6046258
child 29265 5b4247055bd7
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 29 10:58:04 2008 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 29 11:46:47 2008 +0200
     1.3 @@ -557,7 +557,7 @@
     1.4    | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
     1.5    | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
     1.6    | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 => 
     1.7 -      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
     1.8 +      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
     1.9    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    1.10    | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
    1.11    | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)