An axiomatic description with no declaration has the same effect as the corresponding Z constraint paragraph. (In the processing of terms, there were many places where an axiomatic description with an empty declaration could be mapped to the existing constraint paragraph support, if at all. I took the view that the distinction between axiomatic descriptions and constraints was useful at the abstract level because they work differently with the ProofPower theory support so that support for constraints would probably remain. However, the concrete-level support (parsing, syntax trees) is now redundant and, not being in the Standard, I thought it may become deprecated at some point. Thus the implementation only uses the existing abstract level support for constraints.)
Note that this patch is relative to my earlier patch pbc.110605 as they involve changes to the same files.
Phil
patch-2.9.1w2.rda.110226.pbc.110605.pbc.110706.txt.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
