# [isabelle] Syntax for theory definitions

Hello,
I'm new to the list so this is probably a well known fact but I could
not find any information...
I want to run Isabelle over some theories developed by another
researcher. I downloaded
the theories but can not run them in Isabelle 2008.
They are of the form
theory Basic_Op_Rules = Basic_Inf_Rules :
section {* Basic properies *}
lemmas kbox = K_BOX[THEN temp_mp];
lemmas kpbox = K_PBOX[THEN temp_mp];
theorem box1 : " H |- BOX(NEXTA A) -> BOX(A -> NEXTA A) "
apply(rule kbox);
apply(rule MWeak);
apply(rule Nec1);
apply(rule t);
done
...
Any comments on how I can run/convert them so that they work in Isabelle 2008?
Thanks a lot.
Devrim

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