Re: [isabelle] Syntax issue: lost between HOL and Isar

On 8/1/2012 7:40 PM, Christian Sternagel wrote:
Here 'case (Suc n)' as well as 'case 0' (above) are part of Isar not HOL. We could also just use 'case 0' and 'case Suc', then it is more clear


Is this right? There's Isar syntax, which is defined in Pure. There's HOL syntax, which is defined using Isar keywords. And there is the HOL logic which is a combination of Isar syntax and HOL syntax.

What I'm thinking about in particular is that the proof of a HOL theorem is a HOL proof, but it may contain Isar commands.


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