* Isar/Pure: fixed 'token_translation' command;
authorwenzelm
Thu Oct 11 21:25:45 2001 +0200 (2001-10-11)
changeset 1172278cf55fd57c6
parent 11721 0d60622b668f
child 11723 2b4a0d630071
* Isar/Pure: fixed 'token_translation' command;
NEWS
     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