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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev