[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.