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



Hi Gottfried,

> Anyway, I kind of understanding the use of class with class, and that
> class is a locale, and the use of locale with locale, but I haven't
> understood the mixing of "locale" with "class" in Groups.thy, so if I
> get a chance to work through Groups.thy, it could be I'll understand it
> better with this knowledge.

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

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.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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