## 14.295 No locally assumed theory includes the rule

Page 766 of 800 |
| Search internet |

Origin: check. Landing-place: diagnose.

**No locally assumed theory includes the following rule: x**

During tactic expansion of the unification tactic , the unification tactic does unitac expansion. When unitac expansion encounters a statement which is used as an axiom or inference rule, the system tries to locate the axiom or inference rule in the theories assumed at that position. The error may indicate that an axiom or inference rule cannot be used in the given context or may indicate that some assumption is missing. To correct the error, start out by locating the error.

Page 766 of 800 |
| Search logiweb.eu |

Copyright © 2010
Klaus Grue,
GRD-2010-01-05