--- a/src/HOLCF/Tr1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Tr1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -77,7 +77,7 @@
(* 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),
@@ -107,7 +107,7 @@
]);
-val trE = prove_goal Tr1.thy
+qed_goal "trE" Tr1.thy
"[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
(fn prems =>
[
@@ -123,7 +123,7 @@
(* 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),