NEWS
changeset 72810 b00ee476151b
parent 72763 3cc73d00553c
child 72837 2c26c283f3ee
equal deleted inserted replaced
72807:ea189da0ff60 72810:b00ee476151b
    84 
    84 
    85 * Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
    85 * Local_Theory.init replaces Generic_Target.init.  Minor INCOMPATIBILITY.
    86 
    86 
    87 
    87 
    88 *** HOL ***
    88 *** HOL ***
       
    89 
       
    90 * Session "Hoare" now provides a total correctness logic as well.
    89 
    91 
    90 * An updated version of the veriT solver is now included as Isabelle
    92 * An updated version of the veriT solver is now included as Isabelle
    91 component. It can be used in the "smt" proof method via "smt (verit)" or
    93 component. It can be used in the "smt" proof method via "smt (verit)" or
    92 via "declare [[smt_solver = verit]]" in the context; see also session
    94 via "declare [[smt_solver = verit]]" in the context; see also session
    93 HOL-Word-SMT_Examples.
    95 HOL-Word-SMT_Examples.