equal
deleted
inserted
replaced
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 