[isabelle-dev] Relations vs. Predicates

[Christian Sternagel]

Sorry for the inconveniences.

On 04/17/2012 11:55 PM, Makarius wrote:
> Here is another follow-up to the relcomp story so far:
>
> changeset: 47508:85c6268b4071
> tag: tip
> user: wenzelm
> date: Tue Apr 17 16:48:37 2012 +0200
> files: doc-src/TutorialI/Sets/Relations.thy
> description:
> updated rel_comp ~> relcomp (cf. e1b761c216ac);
>
> doc-src/TutorialI/Sets/Relations.thy
>
>
> This is only to make the manual compile again.
This one didn't show up during 'isabelle makeall all'. Shouldn't 
documentation be part of "all"? I guess then that a test should also 
include "./Admin/build doc"? Anything else besides

   isabelle makeall all
   ./Admin/build doc

to test a changeset (apart from external dependencies like the AFP)?

> I hope it is not one of
> the theories that need generated latex copied to another place by hand.
Just out of curiosity: what do you mean by the above statement?

> Moreover NEWS in that version has oddities like this:
>
> rel_comp_def ~> rel_comp_unfold
>
> and later
>
> rel_comp_unfold ~> relcomp_unfold
>
>
> In the time immediately before the relase (which is now) the NEWS should
> reflect the perspective for end-users of the official stable system that
> is delivered.
I observed this oddities but left them deliberately since I was not 
aware of the above convention (which is of course very sensible).

cheers

chris