Hi Binyameen | In HOL we can search the theorems in the theories given in the following | link | | http://hol.sourceforge.net/kananaskis-7-helpdocs/help/HOLindex.html | | but in HOL-light, how can we search out the required theorems?
I haven't generated an HTML reference like this for HOL Light's theorems, though I could certainly do something similar if you or others would find it helpful. There is a text version towards the end of the reference manual, starting around page 755 in the current version: http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf You can also do a more focused search for theorems using the "search" command. See the entry in the same manual on page 617 or do the following in HOL Light for more details: help "search";; John. ------------------------------------------------------------------------------ RSA® Conference 2012 Save $700 by Nov 18 Register now! http://p.sf.net/sfu/rsa-sfdev2dev1 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
