# HG changeset patch
# User paulson
# Date 1030962319 -7200
# Node ID 4679359bb218acaeb7a7e9c0321baee58928e1b3
# Parent  855f6bae851edfe8cad0be5e413615844fa1347c
Added missing rewrite rule and some arith examples

diff -r 855f6bae851e -r 4679359bb218 src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Mon Sep 02 11:07:26 2002 +0200
+++ b/src/HOL/Real/real_arith0.ML	Mon Sep 02 12:25:19 2002 +0200
@@ -11,6 +11,7 @@
 (* reduce contradictory <= to False *)
 val add_rules = 
     [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1,
+     real_minus_1_eq_m1, 
      add_real_number_of, minus_real_number_of, diff_real_number_of,
      mult_real_number_of, eq_real_number_of, less_real_number_of,
      le_real_number_of_eq_not_less, real_diff_def,
@@ -118,4 +119,17 @@
 \     ==> 6*a <= 5*l+i";
 by (fast_arith_tac 1);
 qed "";
+
+Goal "a<=b ==> a < b+(1::real)";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "a<=b ==> a-(3::real) < b";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "a<=b ==> a-(1::real) < b";
+by (fast_arith_tac 1);
+qed "";
+
 *)