# HG changeset patch
# User paulson
# Date 931941693 -7200
# Node ID 6920cf9b8623c5ee4c2f14f5b883eee2bade8d80
# Parent  73f681047e5f1cf7fcc2a989e9c2f4c656bc0057
rewrite add1_zle_eq is no longer in the default simpset

diff -r 73f681047e5f -r 6920cf9b8623 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Wed Jul 14 10:40:51 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Wed Jul 14 10:41:33 1999 +0200
@@ -93,6 +93,8 @@
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (constrains_tac 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [add1_zle_eq]));
 by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
 qed "moving_up";