Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I've just donwloaded a new development version of Isabelle and I find
that thms_containing no longer exists.
I've looked at the NEWS and find:
The trouble is, 'find_theorems' doesn't seem to exist either.
Well, actually, its features are extolled at such length that
I assume it exists - but how do I use it?
It's not mentioned in the reference manual (which, incidentally,
still shows thms_containing)
Jeremy
Email Gateway (Aug 17 2022 at 13:46):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Email Gateway (Aug 18 2022 at 11:43):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
This function seems to have disappeared form a very recent development
version of Isabelle. Or, rather, it seems it recently changed its name
to thms_containing_consts, since I apparently changed my own code
accordingly, but now it has disappeared completely.
What has happened to it / what other function has the same or similar
functionality?
regards,
Jeremy
Email Gateway (Aug 18 2022 at 11:43):From: Makarius <makarius@sketis.net>
This ancient way of indexing facts was both very slow to build, and in
fact unused in the past few years. Facts are now stored in a plain
Facts.T table; the following example shows how the 'find_theorems' command
retrieves facts from the context:
fun all_facts_of ctxt =
maps Facts.selections
(Facts.dest (PureThy.all_facts_of (ProofContext.theory_of ctxt)) @
Facts.dest (ProofContext.facts_of ctxt));
The result is just a plain list, without any special indexing.
If you need special-purpose indexing you can use Theory.at_begin or
Theory.at_end hooks to maintain a derived data structure, but this is not
completely trivial.
Makarius
Last updated: May 03 2024 at 08:18 UTC