# [isabelle] About HOL BNF and inner syntax error

```Hi everybody.

I'm really new to Isabelle. This is my second message to the list.
I've been using Isabelle to prove some HasCASL specifications and until now
I only had to use the Isar apply method.
I've already read the Isabelle Tutorial when I started working with the
tool.

Recently I was told that I need to create lemmas over an axiom to put the
last in such a way Isabelle can match it against the actual premises.
I've searched for a HOL BNF but I could not find it. I need to know what
exactly can be written in lemma/theorems, inside double quotes (the lemma
itself). I took a look in the logics-HOL.pdf but I didn't find the BNF, only
rules of the logic. As I'm not sure if I'm looking for HOL inner syntax or
Isar syntax, I had to ask you some help to find the right doc.

The motivation to get the BNF is this:
I have this axiom:
EqualTransT [rule_format] :
"ALL x.
ALL y.
ALL z. x ==' y = True' & y ==' z = True' --> x ==' z = True'"

And I need to prove this goal:
1. (!!(x (y z)).
([| ((x ==' y) = True'); ((y ==' z) = True');
((x <' z) = False');
((x ==' z) = False') |]
==> False))

I thought I should write some lemma as this one:
lemma L1:
"ALL x.
ALL y.
ALL z.
[| [|(x ==' y) = True' ; (y ==' z) = True'|] ==> (x ==' z) = True'; (x =='
z) = False'|]==> False"

but I always get an inner syntax error and I cannot see where the error is.

Even this lemma cannot pass:
lemma L1:
"ALL x.
ALL z.
[| (x ==' z) = True'; (x ==' z) = False'|] ==> False"

So I guess I need some doc to learn the correct HOL inner syntax (I guess)