[isabelle-dev] Relations vs. Predicates
c-sterna at jaist.ac.jp
Wed Apr 18 03:35:11 CEST 2012
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
> updated rel_comp ~> relcomp (cf. e1b761c216ac);
> 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
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).
More information about the isabelle-dev