Re: [isabelle] Modify theorem with equality assumption



On Tue, 7 Apr 2015, Manuel Eberl wrote:

"The" repository version is undefined, until "hg id" is used.
e83ecf0a0ee1. I usually make a point of pulling the latest version
regularly to keep my developments up-to-date.

"The latest" is only meaningful for an instant of time in your private context that nobody else knows about. Any public discussion on it is invalidated rather quickly, by new incoming changes. Luckily Mercurial has a unique value-oriented id for arbitrary points in history.

"Latest" versions also have the tendency to become outdated rather quickly, paradoxically to become older than the truely latest release version.


Another variation: fix q locally, then work with non-schematic
material inside the extended context (which is usually easier and more
robust), then export the result into the original context to make q
schematic.
Is that not what I did in the end? (q being p')

Ah, I did not see that. Maybe I was confused by the many p', p''. The system already takes care of renamings, so if you mean a local "x" you fix that and call it x in ML. If you mean p' you call it p' etc.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.