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