File Value.ML

open Value;

qed_goalw "the_Addr_Addr" thy [the_Addr_def] 
	"the_Addr (Addr a) = a" (K [Auto_tac]);
Addsimps [the_Addr_Addr];