author | paulson |
Tue, 18 Dec 2001 15:04:19 +0100 | |
changeset 12537 | f2cda6fb1c9f |
parent 12536 | e9a729259385 |
child 12538 | 150af0a4bb11 |
--- 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];