Re: [isabelle] Proof_Context abstraction



Dear Lars,


Am Mittwoch, den 30.07.2014, 08:15 +0200 schrieb Lars Hupel:
> > there is always a first step, and different people learn in different
> > ways. I could have said “experimentation” if you like that word better.
> 
> I found that reading the sources and experimenting (in a type-driven
> way) with them worked well for me. Also, the Isar Implementation Manual
> and the Isabelle/ML Cookbook are valuable resources.

thanks; looks like I’m on the right paths.

Since you mention type-driven: Do you know of a way of having the system
tell me the types of non-exported functions in existing ML code in
Pure/? The exported functions have their types visible in the signature
specification. And for code in my own modules Ctrl-Hover is very
helpful, but that doesn’t work in ML files that have been loaded in the
heap. Is there maybe a way to get jEdit process Pure (instead of loading
a Heap)?


> > So can I expect guidance from those on this list who already spent the
> > long time of study? Or is it expected for newcomers to study on their
> > own until they achieve mastery (or give up)?
> 
> I'm sure you'll find helpful answers here.

Great. Then let me try to ask better questions next times :-)

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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