# HG changeset patch # User lcp # Date 797163327 -7200 # Node ID 2317b680fe586f13e8b3a30a0fd65576b7f488cc # Parent 75110179587d3d8e2a1db4cfb813298279a5a6f7 Now the classical sets include UN_E, to avoid calling hyp_subst_tac diff -r 75110179587d -r 2317b680fe58 src/ZF/ZF.ML --- a/src/ZF/ZF.ML Thu Apr 06 12:11:05 1995 +0200 +++ b/src/ZF/ZF.ML Thu Apr 06 12:15:27 1995 +0200 @@ -411,11 +411,14 @@ swap_res_tac [minor] 1, assume_tac 1 ]); -(*A claset that leaves <= formulae unchanged!*) +(*A claset that leaves <= formulae unchanged! + UN_E appears before UnionE so that it is tried first, to avoid expensive + calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: + would enlarge the search space.*) val subset0_cs = FOL_cs addSIs [ballI, InterI, CollectI, PowI, empty_subsetI] addIs [bexI, UnionI, ReplaceI, RepFunI] - addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE, + addSEs [bexE, make_elim PowD, UN_E, UnionE, ReplaceE2, RepFunE, CollectE, emptyE] addEs [rev_ballE, InterD, make_elim InterD, subsetD];