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
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