8.5.2 The unification tactic

Prev Up Next Page 327 of 800 Search internet

Proof lines which argue if favor of a conclusion are tactic expanded by the unification tactic. The unification tactic is by far the most complicated among the proof tactics defined on the check page.

The unification tactic has its own system of unitac tactics. The unitac aspect of a construct defines how the construct behaves inside an argumentation. As an example, the tactic and unitac definitions of the cut operation x ;; y read:

unitac define x ;; y as \ u . unitac-cut ( u ) end define

tactic define x ;; y as \ u . tactic-cut ( u ) end define

That defines how the cut operation behaves inside and outside argumentations.

Prev Up Next Page 327 of 800 Search logiweb.eu

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