Re: [isabelle] How do I do stone age interaction?

Historically, I see it like this. By 1989, we had the basics: higher-order unification as the inference mechanism and higher-order logic as the logical framework. A couple of years later, we had order-sorted polymorphism. By around 2000, with innovations such as axiomatic type classes, inductive and datatype definitions and the classical reasoner, classic Isabelle could be described as mature. Isar represents a new departure, but what is particularly nice is how well it fits on the old logical framework infrastructure. One might imagine that everything had been foreseen at the start, but this isn't true at all. All this is to say that “to understand Isabelle" could refer to many very different things.

On 8 Dec 2010, at 09:19, Alexander Krauss wrote:

> Dear stone age enthusiasts and others,
> In the present discussions, there seem to be some misunderstandings
> due to conflating two meanings of the word 'Isar'...

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