The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
longer need class numeral_ring. This made a number of special
simp-thms redundant.
(* $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"
| Act "\<guillemotleft>mvar\<guillemotright>trm" ("Act [_]._" [100,100] 100)
end