changeset 8099 | 6a087be9f6d9 |
parent 7355 | 4c43090659ca |
child 9158 | 084abf3d0eff |
--- a/src/FOL/cladata.ML Wed Jan 05 11:50:13 2000 +0100 +++ b/src/FOL/cladata.ML Wed Jan 05 11:50:55 2000 +0100 @@ -20,8 +20,8 @@ end; structure Cla = ClassicalFun(Classical_Data); -structure BasicClassical: BASIC_CLASSICAL = Cla; -open BasicClassical; +structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; +structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]); (*Better for fast_tac: needs no quantifier duplication!*)