NEWS
changeset 72987 b1be35908165
parent 72972 31ff3c962937
child 72996 cdcd2785db94
equal deleted inserted replaced
72986:d231d71d27b4 72987:b1be35908165
   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.