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

On Mon, 27 Jul 2009, Christian Urban wrote:

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

These are just some superficial things that are detected when recompiling the tutorial. The main point is that a development snapshot is more or less undefined, with many potential problems lurking. (Of course I know many of them right now. Proper consolidation will take place for official releases, and usually takes about 6-8 weeks.)

Maybe Christian can point out a version (with changeset id) of the programming tutorial that works with the real Isabelle2009 version.


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