I should have said '@' instead of '?' here. The constant '?' is actually defined in these axiomatisations (using '@').
Mark. on 21/3/14 9:10 AM, Mark Adams <m...@proof-technologies.com> wrote: > ... In HOL Light's axiomatisation, the only such entities are the 'bool' and > 'fun' type constants and the '=' constant (the other axiomatisations also > have the '==>' and '?' constants).... ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/13534_NeoTech _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
