[isabelle-dev] Checked "assume" command

[Tobias Nipkow]

Am 05/09/2012 14:45, schrieb Lars Noschinski:
> I like this goal; but, as you said, this is a long term process and a solution
> to this particular issue does not need more then a `peepwhole view`. We also
> don't deviate much from existing practice, as "show" does a similar trick already.

Let me give you some historic background on "show". Until 2005, you could state
any proposition with "show", just like with "have". This lead users time and
time again into the situation where they stated a wrong show proposition and
wasted time figuring that out. Eventually the great wizard had compassion with
his people, inserted the check you refer to, and a sigh of relief went through
his realm. Of course his people had not made the mistake back then to suggest an
actual change to the holy sources.

Tobias