Comments on v0.95 - ill-formedness of terms

[Till Mossakowski <till@informatik.uni-bremen.de>]

For somebody who just begins to learn about CASL, it seems to be not 
so clear how predicate subsorts do influence (un-)decidability of type
inference.
Of course, the summary is not the place to write rationales, but 
I think it would improve understandability just to extend the 
second paragraph of section 3
"But terms ... are rejected as ill-formed" by something like:

"While {\em well-formedness} of terms of the language can be checked
statically, the question whether a well-formed term actually
represents a value (i.e. the question of {\em definedness}), has
to be checked by the proof system (and it is not decidable in general)."

Perhaps the whole paragraph should be moved to section 4, since section
3 does not talk about well- or ill-formed terms at all.

And subsection 4.2 could be extended with:
"Note that a term belonging to the sort s' is generally not
a term of the sort s, but rather a CAST to s (see below) has 
to be applied to it."

Till