| changeset 37735 | 26e673df3fd0 |
| parent 37681 | 6ec40bc934e1 |
| child 37820 | ffaca9167c16 |
--- a/NEWS Wed Jul 07 08:25:21 2010 +0200 +++ b/NEWS Wed Jul 07 08:25:22 2010 +0200 @@ -95,6 +95,10 @@ INCOMPATIBILITY. +* Inductive package: offers new command "inductive_simps" to automatically + derive instantiated and simplified equations for inductive predicates, + similar to inductive_cases. + New in Isabelle2009-2 (June 2010) ---------------------------------