# HG changeset patch
# User paulson
# Date 1008684259 -3600
# Node ID f2cda6fb1c9fed02771d3d2de03446a49df46e88
# Parent  e9a7292593856ae52ad898e585e1d22b8263a0a0
better simplification makes steps redundant

diff -r e9a729259385 -r f2cda6fb1c9f src/ZF/UNITY/UNITY.ML
--- a/src/ZF/UNITY/UNITY.ML	Tue Dec 18 15:03:27 2001 +0100
+++ b/src/ZF/UNITY/UNITY.ML	Tue Dec 18 15:04:19 2001 +0100
@@ -709,8 +709,6 @@
  "F:increasing(A, r, lam s:state. c) <-> F:program & (EX a. a:A)";
 by (auto_tac (claset() addDs [constrains_type RS subsetD],
                simpset() addsimps [INT_iff]));
-by (cut_inst_tac [("F", "F")] Acts_type 1);
-by (auto_tac (claset(), simpset() addsimps [constrains_def]));
 qed "increasing_constant";
 AddIffs [increasing_constant];