Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs
(* Title: HOL/UNITY/Rename.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
Renaming of state sets
*)
Rename = Extend +
constdefs
rename :: "['a => 'b, 'a program] => 'b program"
"rename h == extend (%(x,u::unit). h x)"
end