[isabelle] Syntax for theory definitions


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


Any comments on how I can run/convert them so that they work in Isabelle 2008?

Thanks a lot.

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