diff options
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -19,6 +19,8 @@ Tactics (i.e. library Classical_Prop or Classical) is loaded. - New "Hint Resolve ->" (or "<-") for declaring iff's as oriented hints (wish #2104). +- New introduction patterns "*" for introducing the next block of dependent + variables and "**" for introducing all quantified variables and hypotheses. Tactic Language |
