# [isabelle] How-to define a object logic

Hi all.
I try to define the system S_1^0 of modal logic (according to "Modal Logics"
by Robert Feys) in order to learn the process of adding a new object logic.
Current version is at:
http://www.myjavaserver.com/~nedzelsky/isabelle/ModalS1_0.html
One of the rules of S_1^0 is EQS (substitution of strict equivalents).
I feel my attempt to formalize it is not very satisfactory. One thing which
bother me is that the axioms are written like the following
ax_sub1: "PROP is_subst(P,Q,P,Q)"
instead of simply
ax_sub1: "is_subst(P,Q,P,Q)"
Any suggestions and comments are highly welcome.
Regards,
Michael Nedzelsky

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