--- a/src/HOLCF/Cfun1.ML Fri Feb 03 12:32:14 1995 +0100
+++ b/src/HOLCF/Cfun1.ML Tue Feb 07 11:59:32 1995 +0100
@@ -12,7 +12,7 @@
(* A non-emptyness result for Cfun *)
(* ------------------------------------------------------------------------ *)
-val CfunI = prove_goalw Cfun1.thy [Cfun_def] "(% x.x):Cfun"
+qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
(fn prems =>
[
(rtac (mem_Collect_eq RS ssubst) 1),
@@ -24,13 +24,13 @@
(* less_cfun is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-val refl_less_cfun = prove_goalw Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
+qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun(f,f)"
(fn prems =>
[
(rtac refl_less 1)
]);
-val antisym_less_cfun = prove_goalw Cfun1.thy [less_cfun_def]
+qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def]
"[|less_cfun(f1,f2); less_cfun(f2,f1)|] ==> f1 = f2"
(fn prems =>
[
@@ -43,7 +43,7 @@
(rtac Rep_Cfun_inverse 1)
]);
-val trans_less_cfun = prove_goalw Cfun1.thy [less_cfun_def]
+qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def]
"[|less_cfun(f1,f2); less_cfun(f2,f3)|] ==> less_cfun(f1,f3)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(* lemmas about application of continuous functions *)
(* ------------------------------------------------------------------------ *)
-val cfun_cong = prove_goal Cfun1.thy
+qed_goal "cfun_cong" Cfun1.thy
"[| f=g; x=y |] ==> f[x] = g[y]"
(fn prems =>
[
@@ -64,7 +64,7 @@
(fast_tac HOL_cs 1)
]);
-val cfun_fun_cong = prove_goal Cfun1.thy "f=g ==> f[x] = g[x]"
+qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f[x] = g[x]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -72,7 +72,7 @@
(rtac refl 1)
]);
-val cfun_arg_cong = prove_goal Cfun1.thy "x=y ==> f[x] = f[y]"
+qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f[x] = f[y]"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -86,7 +86,7 @@
(* additional lemma about the isomorphism between -> and Cfun *)
(* ------------------------------------------------------------------------ *)
-val Abs_Cfun_inverse2 = prove_goal Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
+qed_goal "Abs_Cfun_inverse2" Cfun1.thy "contX(f) ==> fapp(fabs(f)) = f"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -99,7 +99,7 @@
(* simplification of application *)
(* ------------------------------------------------------------------------ *)
-val Cfunapp2 = prove_goal Cfun1.thy
+qed_goal "Cfunapp2" Cfun1.thy
"contX(f) ==> (fabs(f))[x] = f(x)"
(fn prems =>
[
@@ -111,7 +111,7 @@
(* beta - equality for continuous functions *)
(* ------------------------------------------------------------------------ *)
-val beta_cfun = prove_goal Cfun1.thy
+qed_goal "beta_cfun" Cfun1.thy
"contX(c1) ==> (LAM x .c1(x))[u] = c1(u)"
(fn prems =>
[