src/HOLCF/Ssum1.ML

 
 (* ------------------------------------------------------------------------ *)
 (* optimize lemmas about less_ssum                                          *)
 (* ------------------------------------------------------------------------ *)
 
-val less_ssum2a = prove_goal Ssum1.thy 
+qed_goal "less_ssum2a" Ssum1.thy 
 	"less_ssum(Isinl(x),Isinl(y)) = (x << y)"
  (fn prems =>
 	[
 	(rtac less_ssum1a 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
-val less_ssum2b = prove_goal Ssum1.thy 
+qed_goal "less_ssum2b" Ssum1.thy 
 	"less_ssum(Isinr(x),Isinr(y)) = (x << y)"
  (fn prems =>
 	[
 	(rtac less_ssum1b 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
-val less_ssum2c = prove_goal Ssum1.thy 
+qed_goal "less_ssum2c" Ssum1.thy 
 	"less_ssum(Isinl(x),Isinr(y)) = (x = UU)"
  (fn prems =>
 	[
 	(rtac less_ssum1c 1),
 	(rtac refl 1),
 	(rtac refl 1)
 	]);
 
-val less_ssum2d = prove_goal Ssum1.thy 
+qed_goal "less_ssum2d" Ssum1.thy 
 	"less_ssum(Isinr(x),Isinl(y)) = (x = UU)"
  (fn prems =>
 	[
 	(rtac less_ssum1d 1),
 	(rtac refl 1),

 
 (* ------------------------------------------------------------------------ *)
 (* less_ssum is a partial order on ++                                     *)
 (* ------------------------------------------------------------------------ *)
 
-val refl_less_ssum = prove_goal Ssum1.thy "less_ssum(p,p)"
+qed_goal "refl_less_ssum" Ssum1.thy "less_ssum(p,p)"
  (fn prems =>
 	[
 	(res_inst_tac [("p","p")] IssumE2 1),
 	(hyp_subst_tac 1),
 	(rtac (less_ssum2a RS iffD2) 1),

 	(hyp_subst_tac 1),
 	(rtac (less_ssum2b RS iffD2) 1),
 	(rtac refl_less 1)
 	]);
 
-val antisym_less_ssum = prove_goal Ssum1.thy 
+qed_goal "antisym_less_ssum" Ssum1.thy 
  "[|less_ssum(p1,p2);less_ssum(p2,p1)|] ==> p1=p2"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("p","p1")] IssumE2 1),

 	(rtac antisym_less 1),
 	(etac (less_ssum2b RS iffD1) 1),
 	(etac (less_ssum2b RS iffD1) 1)
 	]);
 
-val trans_less_ssum = prove_goal Ssum1.thy 
+qed_goal "trans_less_ssum" Ssum1.thy 
  "[|less_ssum(p1,p2);less_ssum(p2,p3)|] ==> less_ssum(p1,p3)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("p","p1")] IssumE2 1),