better simplification makes steps redundant
authorpaulson
Tue Dec 18 15:04:19 2001 +0100 (2001-12-18)
changeset 12537f2cda6fb1c9f
parent 12536 e9a729259385
child 12538 150af0a4bb11
better simplification makes steps redundant
src/ZF/UNITY/UNITY.ML
     1.1 --- a/src/ZF/UNITY/UNITY.ML	Tue Dec 18 15:03:27 2001 +0100
     1.2 +++ b/src/ZF/UNITY/UNITY.ML	Tue Dec 18 15:04:19 2001 +0100
     1.3 @@ -709,8 +709,6 @@
     1.4   "F:increasing(A, r, lam s:state. c) <-> F:program & (EX a. a:A)";
     1.5  by (auto_tac (claset() addDs [constrains_type RS subsetD],
     1.6                 simpset() addsimps [INT_iff]));
     1.7 -by (cut_inst_tac [("F", "F")] Acts_type 1);
     1.8 -by (auto_tac (claset(), simpset() addsimps [constrains_def]));
     1.9  qed "increasing_constant";
    1.10  AddIffs [increasing_constant];
    1.11