NEWS
 changeset 16000 786c5f838b0c parent 15979 c81578ac2d31 child 16013 3010430d894d
equal inserted replaced
15999:d06fc840a34c 16000:786c5f838b0c
`    87   primes instead of base 26 numbers.`
`    87   primes instead of base 26 numbers.`
`    88 `
`    88 `
`    89 * Pure: new flag show_question_marks controls printing of leading`
`    89 * Pure: new flag show_question_marks controls printing of leading`
`    90   question marks in schematic variable names.`
`    90   question marks in schematic variable names.`
`    91 `
`    91 `
`    92 * Pure: new version of thms_containing that searches for a list `
`    92 * Pure: new version of thms_containing that searches for a list of`
`    93   of patterns instead of a list of constants. Available in `
`    93   criteria instead of a list of constants. Known criteria are: intro,`
`    94   ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. `
`    94   elim, dest, name:string, and any term. Criteria can be preceded by`
`    95   Example search: "(_::nat) + _ + _"   "_ ==> _"`
`    95   '-' to select theorems that do not match. Intro, elim, dest select`
`       `
`    96   theorems that match the current goal, name:s selects theorems whose`
`       `
`    97   fully qualified name contain s.  Any other term is interpreted as`
`       `
`    98   pattern and selects all theorem matching the pattern. Available in`
`       `
`    99   ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f.`
`       `
`   100 `
`       `
`   101   Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL."`
`       `
`   102 `
`       `
`   103   prints the last 100 theorems matching the pattern "(_::nat) + _ + _",`
`       `
`   104   matching the current goal as introduction rule and not having "HOL." `
`       `
`   105   in their name (i.e. not being defined in theory HOL).`
`    96 `
`   106 `
`    97 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).`
`   107 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).`
`    98 `
`   108 `
`    99 * Pure/Syntax: pretty pinter now supports unbreakable blocks,`
`   109 * Pure/Syntax: pretty pinter now supports unbreakable blocks,`
`   100   specified in mixfix annotations as "(00...)".`
`   110   specified in mixfix annotations as "(00...)".`