equal
deleted
inserted
replaced
136 also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" |
136 also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" |
137 like in normal math, and corresponding versions for < and for intersection. |
137 like in normal math, and corresponding versions for < and for intersection. |
138 |
138 |
139 * ML: the legacy theory structures Int and List have been removed. They had |
139 * ML: the legacy theory structures Int and List have been removed. They had |
140 conflicted with ML Basis Library structures having the same names. |
140 conflicted with ML Basis Library structures having the same names. |
|
141 |
|
142 * 'refute' command added to search for (finite) countermodels. Only works |
|
143 for a fragment of HOL. The installation of an external SAT solver is |
|
144 highly recommended. See "HOL/Refute.thy" for details. |
|
145 |
141 |
146 |
142 New in Isabelle2003 (May 2003) |
147 New in Isabelle2003 (May 2003) |
143 -------------------------------- |
148 -------------------------------- |
144 |
149 |
145 *** General *** |
150 *** General *** |