1.1 --- a/NEWS Thu Oct 11 19:22:15 2001 +0200
1.2 +++ b/NEWS Thu Oct 11 21:25:45 2001 +0200
1.3 @@ -20,14 +20,16 @@
1.4
1.5 *** Isar ***
1.6
1.7 -* renamed "antecedent" case to "rule_context";
1.8 -
1.9 * improved proof by cases and induction:
1.10 - moved induct/cases attributes to Pure;
1.11 - added 'print_induct_rules' (covered by help item in Proof General > 3.3);
1.12 - generic setup instantiated for FOL and HOL;
1.13 - removed obsolete "(simplified)" and "(stripped)" options;
1.14
1.15 +* Pure: renamed "antecedent" case to "rule_context";
1.16 +
1.17 +* Pure: fixed 'token_translation' command;
1.18 +
1.19 * HOL: 'recdef' now fails on unfinished automated proofs, use
1.20 "(permissive)" option to recover old behavior;
1.21