[isabelle] HELP



Hello,
here is a coq codes
==============================
Variable line: Set.
Variable parallel:line -> line -> bool.

Variable intersect: line -> line -> bool.
Variable angle : line -> line -> nat.

Hypothesis  axiom1: forall l1 l2:line,
 parallel l1 l2 = true -> angle l1 l2 =0.

Hypothesis axiom2 : forall l1 l2:line,
 angle l1 l2 =0 -> intersect l1 l2 = false.

Lemma parrallel_not_intersect: forall l1 l2:line,
 parallel l1 l2 = true -> intersect l1 l2 = false.
intros.
assert (parallel l1 l2 = true -> intersect l1 l2 = false).
intro;apply axiom2;apply axiom1;assumption.
apply H0.
auto.
Qed.
===========================================
please can anyone give me a hint how to convert this coq codes to
Isabelle/HOL.
Thanks
 Adamu



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