[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