14.295 No locally assumed theory includes the rule

Prev Up Next 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 x conclude y, 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.

Prev Up Next Page 766 of 800 Search logiweb.eu

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