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];

qed_goalw "the_Intg_Intg" thy [the_Intg_def] 
	"the_Intg (Intg i) = i" (K [Auto_tac]);
Addsimps [the_Intg_Intg];