[ProofPower] Re: ".doc" version of Z Reference Manual

[Roger Bishop Jones]

On Monday 13 September 2004 10:28 am, Stephen Brackin wrote:

> Am I correct in gathering that "KWIC" abbreviates "keyword in
> context" and that this index is also called the "KEYWORD
> INDEX"?

Yes and possibly.

> I'm trying to prove something about a function that I defined
> in terms of the %fcompose% symbol, so I wanted to know all the
> theorems and conversions that Lemma1 provides involving this
> symbol.  I found some references to this symbol in the keyword
> index, but hoped there were more.  I looked at the source,
> found usr30.doc, and found that it is mostly "include"
> commands that include .tex files.  These .tex files came from
> .doc files, didn't they?

Yes, mostly extracted from dtd???.doc files.
There is no direct correspondence between the names of the
include files and the names of the dtd's from which they
were derived.

> If so, would Lemma1 be willing to
> provide the .doc files for the purpose of helping people make
> searches involving extended characters?

They are in the distribution, in the src directory.

Its probably better to cook up a function to search the
theory database, e.g.:

fun const_thms tm =
let	val (cn, _) = dest_const tm;
	fun aux1 th = map (fn (k,t)=> ((th,hd k),t)) (get_thms th);
	fun aux2 (x,y) = cn mem (map fst (term_consts (concl y)));
in filter aux2 (flat (map aux1 (get_ancestors "-")))
end;

The KWIC index is still the best place to look for the 
conversions.

Roger Jones