--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 19:21:51 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Apr 05 19:21:51 2009 +0100
@@ -657,6 +657,7 @@
fun dest_frac ct = case term_of ct of
Const (@{const_name "HOL.divide"},_) $ a $ b=>
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
fun mk_frac phi cT x =
--- a/src/HOL/Library/normarith.ML Sun Apr 05 19:21:51 2009 +0100
+++ b/src/HOL/Library/normarith.ML Sun Apr 05 19:21:51 2009 +0100
@@ -369,6 +369,7 @@
fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
@@ -795,8 +796,9 @@
open Conv Thm Conv2;
val bool_eq = op = : bool *bool -> bool
- fun dest_ratconst t = case term_of t of
+ fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
fun augment_norm b t acc = case term_of t of