rewrite add1_zle_eq is no longer in the default simpset
authorpaulson
Wed, 14 Jul 1999 10:41:33 +0200
changeset 7000 6920cf9b8623
parent 6999 73f681047e5f
child 7001 8121e11ed765
rewrite add1_zle_eq is no longer in the default simpset
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";