aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorArnaud Spiwack2014-07-31 16:57:23 +0200
committerArnaud Spiwack2014-08-01 19:18:59 +0200
commitb240b7d0cfd6233dcb0ba0e3b98354c78c23a0d4 (patch)
treefdea52e140e7aec2d18b4a26b734c335a990037c
parentd9e39315b0debcb6c8cd95821db19f83364b263f (diff)
CHANGES: [>…].
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2d5216d6b7..ac76b9eca5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -99,6 +99,7 @@ Tactics
* New tactic language feature "numgoals" to count number of goals.
Accompanied by "guard" tactic which fails if a boolean test does
not pass.
+ * New tactical "[> ... ]" to apply tactics to individual goals.
* The refine tactic is changed not to use an ad hoc typing algorithm
to generate subgoals. It also uses the dependent subgoal feature
to generate goals to materialise every existential variable which