author | wenzelm |

Thu Mar 19 11:20:22 2009 +0100 (2009-03-19) | |

changeset 30577 | 79cc595655c0 |

parent 30576 | 7e5b9bbc54d8 |

child 30578 | 9863745880db |

tuned;

1.1 --- a/NEWS Wed Mar 18 22:41:15 2009 +0100 1.2 +++ b/NEWS Thu Mar 19 11:20:22 2009 +0100 1.3 @@ -176,30 +176,28 @@ 1.4 * The 'axiomatization' command now only works within a global theory 1.5 context. INCOMPATIBILITY. 1.6 1.7 -* New find_theorems criterion "solves" matching theorems that directly 1.8 -solve the current goal. Try "find_theorems solves". 1.9 - 1.10 -* Added an auto solve option, which can be enabled through the 1.11 -ProofGeneral Isabelle settings menu (disabled by default). 1.12 - 1.13 -When enabled, find_theorems solves is called whenever a new lemma is 1.14 -stated. Any theorems that could solve the lemma directly are listed 1.15 -underneath the goal. 1.16 - 1.17 -* New command 'find_consts' searches for constants based on type and 1.18 -name patterns, e.g. 1.19 +* New 'find_theorems' criterion "solves" matching theorems that 1.20 +directly solve the current goal. 1.21 + 1.22 +* Auto solve feature for main theorem statements (cf. option in Proof 1.23 +General Isabelle settings menu, enabled by default). Whenever a new 1.24 +goal is stated, "find_theorems solves" is called; any theorems that 1.25 +could solve the lemma directly are listed underneath the goal. 1.26 + 1.27 +* Command 'find_consts' searches for constants based on type and name 1.28 +patterns, e.g. 1.29 1.30 find_consts "_ => bool" 1.31 1.32 By default, matching is against subtypes, but it may be restricted to 1.33 -the whole type. Searching by name is possible. Multiple queries are 1.34 +the whole type. Searching by name is possible. Multiple queries are 1.35 conjunctive and queries may be negated by prefixing them with a 1.36 hyphen: 1.37 1.38 find_consts strict: "_ => bool" name: "Int" -"int => int" 1.39 1.40 -* New command 'local_setup' is similar to 'setup', but operates on a 1.41 -local theory context. 1.42 +* Command 'local_setup' is similar to 'setup', but operates on a local 1.43 +theory context. 1.44 1.45 1.46 *** Document preparation ***