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 
reference manual.


> 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.

Cheers,
Gerwin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.