Hi Felix, Many of your questions have been well answered already by Petros and Mark, but here are some comments on two items:
| 2) Where are definitions stored, anyway? There seems to be some global | state involved. Is there a way to make definitions locally? Or to pass | definitions around explicitly? At the moment, the definitions are just stored in a mutable list, as you say. The actual variable (see "the_definitions" in fusion.ml) is buried in the logical kernel but you can inspect it by "definitions()", and of course it gets extended when you make a definition. In some ways it would be more elegant to remove such uses of mutable state, which can probably be done without significantly compromising simplicity or efficiency. See for example Freek Wiedijk's "Stateless HOL" paper: http://arxiv.org/abs/1103.3322v1 | 3) HOL Light has large libraries for num, int and real. Are there also | libraries for abstract groups, rings or fields? Not in the standard distribution, anyway, though some people may well have developed their own. Generally the mathematical theories included in the core distribution are biased towards specific structures rather than general axiomatic theories. John. ------------------------------------------------------------------------------ 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
