--- a/Prod.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Prod.ML Fri Nov 25 09:12:16 1994 +0100
@@ -67,7 +67,7 @@
qed "Pair_fst_snd_eq";
(*Prevents simplification of c: much faster*)
-val split_weak_cong = prove_goal Prod.thy
+qed_goal "split_weak_cong" Prod.thy
"p=q ==> split(c,p) = split(c,q)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
@@ -152,12 +152,12 @@
(*** Disjoint union of a family of sets - Sigma ***)
-val SigmaI = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaI" Prod.thy [Sigma_def]
"[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
(*The general elimination rule*)
-val SigmaE = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaE" Prod.thy [Sigma_def]
"[| c: Sigma(A,B); \
\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
\ |] ==> P"
@@ -166,17 +166,17 @@
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
-val SigmaD1 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> a : A"
+qed_goal "SigmaD1" Prod.thy "<a,b> : Sigma(A,B) ==> a : A"
(fn [major]=>
[ (rtac (major RS SigmaE) 1),
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
-val SigmaD2 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
+qed_goal "SigmaD2" Prod.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
(fn [major]=>
[ (rtac (major RS SigmaE) 1),
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
-val SigmaE2 = prove_goal Prod.thy
+qed_goal "SigmaE2" Prod.thy
"[| <a,b> : Sigma(A,B); \
\ [| a:A; b:B(a) |] ==> P \
\ |] ==> P"