equal
deleted
inserted
replaced
176 - Use veriT in proof preplay. |
176 - Use veriT in proof preplay. |
177 - Take adventage of more cores in proof preplay. |
177 - Take adventage of more cores in proof preplay. |
178 |
178 |
179 * Syntax for state monad combinators fcomp and scomp is organized in |
179 * Syntax for state monad combinators fcomp and scomp is organized in |
180 bundle state_combinator_syntax. Minor INCOMPATIBILITY. |
180 bundle state_combinator_syntax. Minor INCOMPATIBILITY. |
|
181 |
|
182 * Syntax for reflected term syntax is organized in bundle term_syntax, |
|
183 discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. |
181 |
184 |
182 |
185 |
183 *** FOL *** |
186 *** FOL *** |
184 |
187 |
185 * Added the "at most 1" quantifier, Uniq, as in HOL. |
188 * Added the "at most 1" quantifier, Uniq, as in HOL. |