NEWS
changeset 6922 f5c5b81b3f14
parent 6795 35f214e73668
child 6925 8d4d45ec6a3d
equal deleted inserted replaced
6921:78a2ce8fb8df 6922:f5c5b81b3f14
     4 
     4 
     5 New in this Isabelle version
     5 New in this Isabelle version
     6 ----------------------------
     6 ----------------------------
     7 
     7 
     8 *** Overview of INCOMPATIBILITIES (see below for more details) ***
     8 *** Overview of INCOMPATIBILITIES (see below for more details) ***
       
     9 
       
    10 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
       
    11 are no longer simplified.  (This allows the simplifier to unfold recursive
       
    12 functional programs.)  To restore the old behaviour, declare
       
    13 	Delcongs [if_weak_cong];
     9 
    14 
    10 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
    15 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
    11 complement;
    16 complement;
    12 
    17 
    13 * HOL: the predicate "inj" is now defined by translation to "inj_on";
    18 * HOL: the predicate "inj" is now defined by translation to "inj_on";
    99 simplifier.
   104 simplifier.
   100 
   105 
   101 NB: At the moment, these decision procedures do not cope with mixed
   106 NB: At the moment, these decision procedures do not cope with mixed
   102 nat/int formulae where the two parts interact, such as `m < n ==>
   107 nat/int formulae where the two parts interact, such as `m < n ==>
   103 int(m) < int(n)'.
   108 int(m) < int(n)'.
       
   109 
       
   110 * Integer division and remainder can now be performed on constant arguments.  
       
   111 
       
   112 * Many properties of integer multiplication, division and remainder are now
       
   113 available.
   104 
   114 
   105 * New bounded quantifier syntax (input only):
   115 * New bounded quantifier syntax (input only):
   106   ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
   116   ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
   107 
   117 
   108 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
   118 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization