New in Yarrow v1.20 (since v1.00)
Yarrow now supports forward reasoning, with the 'Forward' tactic.
Yarrow now supports records and subtyping.
Other significant changes
It is possible to declare a variable as 'Binder', which makes terms better
All commands and tactics have become case-insensitive, e.g. you can type
'Intros' or 'InTrOs' instead of 'Intros'.
- The 'Undo' command is now local, i.e. it undoes the last step in the
current goal instead of the absolute last step. As a consequence,
no tactics can be undone if the goal is proved.
The 'History' command is adapted accordingly, it also prints the tactics
in a more structured way.
It is now possible to suppress printing of selected elements of the local
context, with the tactic 'Hide'. The tactic 'Unhide' makes the
- The tactics 'ExistsE', 'ExistsI', 'Refl', 'Rewrite' and 'Lewrite' have been
flexible: The existential quantification and the equality predicate
can be arbitrarily polymorphic (including not polymorphic at all)
- The tactics Rewrite and Lewrite can also be used in hypotheses.
The special tactics 'AndEL' and 'AndER' replace the old 'AndE' tactic.
This is still available; it is a combination of 'AndEL' and 'AndER'.
- The 'Focus' command is no longer a tactic.
- The tactical 'Then' has been made more flexible.
- A new tactical 'Else'.
- Also if a line ends with ':=', the command may be completed on the next
- 'Prove @x1,x2:Nat. P x1 x2' and then 'Intros' lead to variables 'x' and
'x1' in the context instead of 'x1' and 'x2'.
- During the summary of the used tactics, terms were sometimes printed
in an awkward way, e.g. 'convert (=) x y'.
- The matching routine sometimes gave an internal error. This resulted
sometimes in internal errors when using 'Apply' or rewriting tactics.
- The tactic 'Pattern' sometimes resulted in an ill-typed goal. Now any
attempt to do so results in an error.
Back to Yarrpw Releases Page
Back to Yarrow Home Page