A patch that adds support for empty schema paragraphs is attached. This allows schema definitions and axiomatic descriptions to have an empty declaration. (The present support for empty schemas does not extend to paragraphs.)

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.


Attachment: patch-2.9.1w2.rda.110226.pbc.110605.pbc.110706.txt.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to