Thanks to everyone who wrote about my seg< problem! Just knowing that folks are willing to answer my questions really encourages me, because I know there's a lot I don't know.
Freek, that's very interesting! Evaluating this in HOL Light # help "new_definition";; gives more information than is in the HOL Light Reference manual: FAILURE CONDITIONS new_definition fails if c is already a constant or if the definition does not have the right form. That's what I needed to understand, and it's not in http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/new_definition.html Your other suggestion # help "new_constant";; also lists a failure condition not in the manual: FAILURE CONDITIONS Fails if there is already a constant of that name in the current theory. So I'll use the help feature when I get error messages! Ramana, I have not yet read HOL Logic manual as you suggested on the Isabelle group, but it sounds like a good idea, especially as I did not find the Old user manual on the HOL Light web page very helpful. -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
