Re: [isabelle] thms_containing
On Wednesday 22 February 2006 10:47, Jeremy Dawson wrote:
> * Command 'thms_containing' has been discontinued in favour of
> 'find_theorems'; INCOMPATIBILITY.
> The trouble is, 'find_theorems' doesn't seem to exist either.
find_theorems is a user-level Isar command. It is explained in the Isar
> Well, actually, its features are extolled at such length that
> I assume it exists - but how do I use it?
I assume you want to use it from the ML level. You can find it in
Pure/Isar/find_theorems.ML, usage corresponds closely to the Isar level
description, although it is not actually thought to be used directly from
the ML level (but it's possible, of course).
> It's not mentioned in the reference manual (which, incidentally,
> still shows thms_containing)
The reference manual is kept up to date for releases, it usually lags behind
for the development version.
This archive was generated by a fusion of
Pipermail (Mailman edition) and