Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
(* $Id$ *)
theory Lambda_mu
imports "../Nominal"
begin
section {* Lambda-Mu according to a paper by Gavin Bierman *}
atom_decl var mvar
nominal_datatype trm =
Var "var"
| Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
| App "trm" "trm"
| Pss "mvar" "trm" (* passivate *)
| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100) (* activate *)
end