NEWS
changeset 62027 b270f2b9bef8
parent 62026 ea3b1b0413b4
child 62031 8b50da907602
equal deleted inserted replaced
62026:ea3b1b0413b4 62027:b270f2b9bef8
    84 
    84 
    85 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
    85 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
    86 instead of former C+e LEFT.
    86 instead of former C+e LEFT.
    87 
    87 
    88 * The command-line tool "isabelle jedit" and the isabelle.Main
    88 * The command-line tool "isabelle jedit" and the isabelle.Main
    89 application wrapper threat the default $USER_HOME/Scratch.thy more
    89 application wrapper treat the default $USER_HOME/Scratch.thy more
    90 uniformly, and allow the dummy file argument ":" to open an empty buffer
    90 uniformly, and allow the dummy file argument ":" to open an empty buffer
    91 instead.
    91 instead.
    92 
    92 
    93 * New command-line tool "isabelle jedit_client" allows to connect to an
    93 * New command-line tool "isabelle jedit_client" allows to connect to an
    94 already running Isabelle/jEdit process. This achieves the effect of
    94 already running Isabelle/jEdit process. This achieves the effect of
   549   - Fixed soundness bug in translation of "finite" predicate.
   549   - Fixed soundness bug in translation of "finite" predicate.
   550   - Fixed soundness bug in "destroy_constrs" optimization.
   550   - Fixed soundness bug in "destroy_constrs" optimization.
   551   - Removed "check_potential" and "check_genuine" options.
   551   - Removed "check_potential" and "check_genuine" options.
   552   - Eliminated obsolete "blocking" option.
   552   - Eliminated obsolete "blocking" option.
   553 
   553 
   554 * New (co)datatype package:
   554 * (Co)datatype package:
   555   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
   555   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
   556     structure on the raw type to an abstract type defined using typedef.
   556     structure on the raw type to an abstract type defined using typedef.
   557   - Always generate "case_transfer" theorem.
   557   - Always generate "case_transfer" theorem.
   558   - Allow discriminators and selectors with the same name as the type
   558   - Allow discriminators and selectors with the same name as the type
   559     being defined.
   559     being defined.