define pyk of axiom mp as text unicode start of text unicode small a unicode small x unicode small i unicode small o unicode small m unicode space unicode small m unicode small p unicode end of text end unicode text end text end define
define tex of axiom mp as text unicode start of text unicode capital m unicode capital p unicode end of text end unicode text end text end define
define statement of axiom mp as propositional theory infer all metavar var a end metavar indeed all metavar var b end metavar indeed ( metavar var a end metavar infer ( ( metavar var a end metavar imply metavar var b end metavar ) infer metavar var b end metavar ) ) end define
define proof of axiom mp as rule tactic end define
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,