On 14/02/11 06:39, Lu Zhao wrote:
> val rel1_def =
> Define `rel1 (u:word32) v x y z = v x y z /\ x /\ y u /\ z`;
>
> val V_OK_def = Define `V_OK x y z = T`;
>
> Hol_reln `
> (!p c q. rel1 u V_OK p c q ==> rel2 u p c q) /\
> (!p c q. rel1 u (rel2 u) p c q ==> rel2 u p c q)`
This is a per
Hi,
I'm having the following error when I attempt to define a relation with
Hol_reln:
Exception raised at IndDefLib.Hol_reln:
at IndDefLib.Hol_mono_reln:
at IndDefRules.derive_strong_induction:
at Thm.EQ_MP:
The failure of "derive_strong_induction" happens for a situation like
the following. I
