NEWS
changeset 14624 9b3397a848c3
parent 14610 9c2e31e483b2
child 14655 8a95abf87dd3
equal deleted inserted replaced
14623:811c09d426cc 14624:9b3397a848c3
    97 * HOL: Tactic emulation methods induct_tac and case_tac understand static
    97 * HOL: Tactic emulation methods induct_tac and case_tac understand static
    98   (Isar) contexts.
    98   (Isar) contexts.
    99 
    99 
   100 
   100 
   101 *** HOL ***
   101 *** HOL ***
       
   102 
       
   103 * Proof import: new image HOL4 contains the imported library from
       
   104   the HOL4 system with about 2500 theorems. It is imported by
       
   105   replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
       
   106   can be used like any other Isabelle image.  See
       
   107   HOL/Import/HOL/README for more information.
   102 
   108 
   103 * Simplifier:
   109 * Simplifier:
   104   - Much improved handling of linear and partial orders.
   110   - Much improved handling of linear and partial orders.
   105     Reasoners for linear and partial orders are set up for type classes
   111     Reasoners for linear and partial orders are set up for type classes
   106     "linorder" and "order" respectively, and are added to the default simpset
   112     "linorder" and "order" respectively, and are added to the default simpset