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

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.

  Michael Nedzelsky

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