diff -r 0d60622b668f -r 78cf55fd57c6 NEWS --- a/NEWS Thu Oct 11 19:22:15 2001 +0200 +++ b/NEWS Thu Oct 11 21:25:45 2001 +0200 @@ -20,14 +20,16 @@ *** Isar *** -* renamed "antecedent" case to "rule_context"; - * improved proof by cases and induction: - moved induct/cases attributes to Pure; - added 'print_induct_rules' (covered by help item in Proof General > 3.3); - generic setup instantiated for FOL and HOL; - removed obsolete "(simplified)" and "(stripped)" options; +* Pure: renamed "antecedent" case to "rule_context"; + +* Pure: fixed 'token_translation' command; + * HOL: 'recdef' now fails on unfinished automated proofs, use "(permissive)" option to recover old behavior;