Dear Members of the Research Community,
A frequent and ongoing impediment in mathematical research is an only partial
understanding of the nature of antinomies, in which _self-reference_ is
(correctly) identified as a characteristic of the antinomy, but in which it is
also omitted that - as is
If you understand what the package is doing (and I admit that this is not
easy), then the behaviour of the simplifier on big records is in turn fairly
understandable.
The advantage of the package is not suffering a quadratic blow-up in elapsed
time and theorem sizes (in turn leading to quadrati
Dear HOL users,
Does anyone know how to use the big record package? I always find I want to
turn it off (by increasing the big record size to above the max number of
fields in my types) because many things don't work on big records (in
particular the simplifier and EVAL) whereas they do work on "s
