Re: [isabelle] ProofGeneral font-lock-mode and antiquoatations



Makarius writes:
 > 
 > BTW, since Christian Urban (who is managing the IDP) is always hooked on 
 > some repository version, readers of the "current" tutorial will need to 
 > learn both Isabelle internals and the very delicate internal development 
 > process at the same time.

The use of "current" for the Programming Tutorial is 
not set in stone. As Markus implied, following "current" has 
its disadvantages. It is the most convenient for me at the 
moment. If contributors of the Tutorial complain enough, I 
am sure I will bend over backwards to accommodate their views. 
As far as readers are concerned, the difference is mostly 
syntactic nature

 stable:         current:

 makestring   -> PolyML.makestring
 import_thms  -> import
 NamedThmsFun -> Named_Thms
 DatatypePackage.get_datatype -> Datatype.get_info
 tctical.ML   -> tactical.ML
 inductive_package.ML -> inductive.ML

If the ride gets bumpier, I will think of something.

Best wishes,
Christian





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