Ramana writes: | The Description Manual for HOL4 explains how to use | Hol_reln. I think it would prefer you to define | sigma_sets as a predicate (i.e. without using IN). Of | course, you end up with the same set (since sets and | predicates are the logically the same in HOL).
HOL Light has a variant of the inductive relation command called "new_inductive_set" (written by Marco Maggesi) that lets you express the definition using "IN". The code is a wrapper around the existing command and is not all that long (see the end of "sets.ml"). If there is enough interest in inductive definitions of sets, it might be worth considering some similar wrapper in HOL4. John. ------------------------------------------------------------------------------ Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
