Re: [isabelle] ProofGeneral font-lock-mode and antiquoatations
> 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and