Re: [isabelle] Isabelle2014-RC0: add_assoc hidden, causes error, but proof passes



On 14-07-12 14:27, Florian Haftmann wrote:
if you want to inspect the theories in HOL-Main interactively, you can
do so by e.g.

	isabelle jedit -l Pure src/HOL/Groups.thy

I've seen that several times, but I always forget about it, so now I've made me a batch file to remind me how to look at single files like that.

Admittedly »cntl-clicking« has its limitations in the presence of »multi
dimensions« which enter the game through locale interpretation.  But to
get a rough idea what is pulled in by »interpretation« or »sublocale«,
issue »print_theorems« directly afterwards.

In a roundabout way that's helped make things a little clearer.

The learning curve of Isabelle isn't linear. It is better described as discontinuous everywhere, so I do searches in docs to find the particular use of some syntax, and then go forwards or backwards.

I haven't find anything like "sublocale add!:", but I finally made the connection to things like "sublocale partial_order < dual!:". Type classes are fairly straight forward, and I have uses for them, but locales aren't as straight forward, and I haven't used them much.

It's not obvious that "interpretation" and "sublocale" should go together. For anyone who hasn't found it, there's this additional PDF about locales by Clemens Ballarin, published in 2014:

http://www4.in.tum.de/~ballarin/publications/jar2013.pdf

of http://www4.in.tum.de/~ballarin/publications/index.html

Regards,
GB




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