aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES1
1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2d5216d6b..ac76b9eca 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