changes to the well-foundedness condition

In accordance with today's decision to relax the constraints on the symbols in
BLD, I have relaxed the conditions for well-foundedness and the corresponding
specialization from FLD - pls see the wiki

I think the decision didn't explicitly mention whether external and plain
function symbols (and likewise predicate symbols) are to be interchangeable or
not. I assumed that they are not, but just wanted to mention this in case
anybody objects.

michael

Received on Wednesday, 25 March 2009 03:41:13 UTC