src/HOLCF/Tr1.ML

 
 (* ------------------------------------------------------------------------ *) 
 (* Exhaustion and elimination for type tr                                   *) 
 (* ------------------------------------------------------------------------ *)
 
-val Exh_tr = prove_goalw Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
+qed_goalw "Exh_tr" Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
  (fn prems =>
 	[
 	(res_inst_tac [("p","rep_tr[t]")] ssumE 1),
 	(rtac disjI1 1),
 	(rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )

 	(contr_tac 1),
 	(atac 1)
 	]);
 
 
-val trE = prove_goal Tr1.thy
+qed_goal "trE" Tr1.thy
 	"[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
  (fn prems =>
 	[
 	(rtac (Exh_tr RS disjE) 1),
 	(eresolve_tac prems 1),

 
 (* ------------------------------------------------------------------------ *) 
 (* type tr is flat                                                          *) 
 (* ------------------------------------------------------------------------ *)
 
-val flat_tr = prove_goalw Tr1.thy [flat_def] "flat(TT)"
+qed_goalw "flat_tr" Tr1.thy [flat_def] "flat(TT)"
  (fn prems =>
 	[
 	(rtac allI 1),
 	(rtac allI 1),
 	(res_inst_tac [("p","x")] trE 1),