accum_sig
and accumulate.
-M flag which can be used to generate
makefile style dependency lists for developments. Also
added examples/makefile which demonstrates a typical
makefile for a development.
search tactic now descends underneath forall and
implication. It now embodies every right rule of the logic.
search tactic.
apply.backchain tactic which is in some sense
dual to the apply tactic. The backchain
tactic applies a lemma (or hypothesis) to the current goal and
produces new subgoals for each of the hypotheses to the lemma.
permute tactic which permutes the nominal
constants in a hypothesis or goal.Quit command.Specification command as
described here.
Query command allows the animation of definitions
as described here.
abella
--help to find out more.
Set command as described
here.
abbrev and unabbrev commands as
described here.
/*
... */. These comments may be nested.
split tactic now operates on n-ary
conjunctionsapplysearch tactic now takes an optional natural
number argument specifying the maximum depth of searching (default
5)CoDefine, which works much
like Define, and the tactic coinduction,
which is similar to induction but takes no arguments. A
brief example of these features is discussed in the Abella reference
guide in the section on
coinductive
restrictions. The following examples are now included in the
distribution of Abella.
Note: The formal meta-logic underlying Abella with
coinduction is still being developed. A paper with the full logic is
forthcoming.
left and right tactics for
selecting the left or right side when the current goal is a
disjunction.exists tactic where nominal
constants were being treated as regular constants.Axiom command since it can be replaced with a
theorem which uses only the skip tactic.
search tactic now does a better job of
backtracking. In particular, each instantiatable variable is now
unbound when the event which caused it to be bound is backtracked
over.search tactic now delays conflict pairs which
fall outside of the pattern unification fragment. Thus this tactic
is now more robust.apply tactic now allows specific instantiations
for variables. The general form is
apply <HYP-NAME> to <HYP-NAMES> with X1 = T1,
..., Xn = Tn.
where the X1 ... Xn are the variables to
be instantiated with T1 ... Tn.
search tactic by
adding some corner cases of unification.search tactic now uses iterative deepening
depth-first search instead of simply depth-first search.