Logiweb(TM)

14.286 Deref tactic used on undefined statement

Prev Up Next Page 757 of 800 Search internet


Origin: check. Landing-place: diagnose.

Deref tactic used on undefined statement: x

The Deref tactic x Deref was applied to an argumentation x whose conclusion was not the name of a lemma, axiom, theory, or similar. The term x is given out of context and after macro and tactic expansion, so start out by locating the error. See also Deref-seqop used on undefined statement.

Prev Up Next Page 757 of 800 Search logiweb.eu

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