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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and