equal
deleted
inserted
replaced
101 * Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY. |
101 * Local_Theory.init replaces Generic_Target.init. Minor INCOMPATIBILITY. |
102 |
102 |
103 |
103 |
104 *** HOL *** |
104 *** HOL *** |
105 |
105 |
106 * Session "Hoare" now provides a total correctness logic as well. |
|
107 |
|
108 * An updated version of the veriT solver is now included as Isabelle |
106 * An updated version of the veriT solver is now included as Isabelle |
109 component. It can be used in the "smt" proof method via "smt (verit)" or |
107 component. It can be used in the "smt" proof method via "smt (verit)" or |
110 via "declare [[smt_solver = verit]]" in the context; see also session |
108 via "declare [[smt_solver = verit]]" in the context; see also session |
111 HOL-Word-SMT_Examples. |
109 HOL-Word-SMT_Examples. |
112 |
110 |
210 * Syntax for state monad combinators fcomp and scomp is organized in |
208 * Syntax for state monad combinators fcomp and scomp is organized in |
211 bundle state_combinator_syntax. Minor INCOMPATIBILITY. |
209 bundle state_combinator_syntax. Minor INCOMPATIBILITY. |
212 |
210 |
213 * Syntax for reflected term syntax is organized in bundle term_syntax, |
211 * Syntax for reflected term syntax is organized in bundle term_syntax, |
214 discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. |
212 discontinuing previous locale term_syntax. Minor INCOMPATIBILITY. |
|
213 |
|
214 * Session "HOL-Hoare": concrete syntax only for Hoare triples, not |
|
215 abstract language constructors. |
|
216 |
|
217 * Session "HOL-Hoare": now provides a total correctness logic as well. |
215 |
218 |
216 |
219 |
217 *** FOL *** |
220 *** FOL *** |
218 |
221 |
219 * Added the "at most 1" quantifier, Uniq, as in HOL. |
222 * Added the "at most 1" quantifier, Uniq, as in HOL. |