* New find_theorems criterion "solves" matching theorems that directly solve the current goal. Try "find_theorems solves".
* Added an auto solve option, which can be enabled through the ProofGeneral Isabelle settings menu (disabled by default). When enabled, find_theorems solves is called whenever a new lemma is stated. Any theorems that could solve the lemma directly are listed underneath the goal. (contributed by Timothy Bourke) Cheers, Gerwin
