--- a/src/HOL/Real/ferrante_rackoff.ML Tue Jun 12 20:49:56 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff.ML Tue Jun 12 21:59:40 2007 +0200
@@ -51,7 +51,7 @@
val context_ss = simpset_of (the_context ());
fun ferrack_tac q i = ObjectLogic.atomize_tac i
- THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, abs_split] i)
+ THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i)
THEN (fn st =>
let
val g = nth (prems_of st) (i - 1)
@@ -61,7 +61,7 @@
(* Some simpsets for dealing with mod div abs and nat*)
val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}]
(* simp rules for elimination of abs *)
- val simpset3 = HOL_basic_ss addsplits [abs_split]
+ val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}]
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
(* Theorem for the nat --> int transformation *)
val pre_thm = Seq.hd (EVERY
--- a/src/HOL/Real/rat_arith.ML Tue Jun 12 20:49:56 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML Tue Jun 12 21:59:40 2007 +0200
@@ -17,7 +17,8 @@
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
- of_int_0, of_int_1, @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
+ @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
+ @{thm of_int_minus}, @{thm of_int_diff},
@{thm of_int_mult}, @{thm of_int_of_nat_eq}]
val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,