equal
deleted
inserted
replaced
69 |
69 |
70 * Clear distinction between types for bits (False / True) and Z2 (0 / |
70 * Clear distinction between types for bits (False / True) and Z2 (0 / |
71 1): theory HOL/Library/Bit.thy has been renamed accordingly. |
71 1): theory HOL/Library/Bit.thy has been renamed accordingly. |
72 INCOMPATIBILITY. |
72 INCOMPATIBILITY. |
73 |
73 |
74 * Fact collection sign_simps contains only simplification rules for |
74 * Fact collections algebra_split_simps and field_split_simps correspond |
75 products being less / greater / equal to zero; combine with existing |
75 to algebra_simps and field_simps but contain more aggressive rules |
76 collections algebra_simps or field_simps to obtain reasonable |
76 potentially splitting goals; algebra_split_simps roughly replaces |
77 simplification. INCOMPATIBILITY. |
77 sign_simps and field_split_simps can be used instead of divide_simps. |
|
78 INCOMPATIBILITY. |
78 |
79 |
79 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) |
80 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) |
80 associates to the left now as is customary. |
81 associates to the left now as is customary. |
81 |
82 |
82 |
83 |