[isabelle-dev] Relations vs. Predicates
Makarius
makarius at sketis.net
Tue Apr 17 16:55:48 CEST 2012
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. I hope it is not one of
the theories that need generated latex copied to another place by hand.
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.
Makarius
More information about the isabelle-dev
mailing list