Michael Norrish
Michael Norrish
Now there are so many traces, the output provided by `traces()` is confusing. I think it would be an improvement to group traces into related areas. ## Want to back...
Something like ``` case v of (x, INL y) => C (f x y) | (a, INR b) => C (g a b) ``` can be simplified to ``` C...
Figure out a nice way for users to be able to provide/define standard total comparison values (of type `α toto`) for the `enumfset` machinery. ## Want to back this issue?...
As with normal `make`, this would allow an invocation that first has Holmake change its working directory and then proceed. ## Want to back this issue? **[Post a bounty on...
I assume this is because repeated invocations of minisat via the `Process.system` is slow. (Or it may be that writing and reading files is slow) My feeling is that the...
`BAG_IN` is redundant in the same way that `MEM` is; we end up proving two sets of theorems: one for `BAG_IN` and one for `SET_OF_BAG`. To be explicit, the overload...
We should gain a deal of build-time efficiency by having multiple theories built within the one Poly/ML session. It's even possible that ``` val _ = export_theory() (* end of...