--- a/src/HOLCF/Cfun2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cfun2.ML Fri May 31 19:55:19 1996 +0200
@@ -48,11 +48,11 @@
(rtac Rep_Cfun 1)
]);
-val monofun_fapp2 = cont_fapp2 RS cont2mono;
+bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
(* monofun(fapp(?fo1)) *)
-val contlub_fapp2 = cont_fapp2 RS cont2contlub;
+bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
(* contlub(fapp(?fo1)) *)
(* ------------------------------------------------------------------------ *)
@@ -60,10 +60,10 @@
(* looks nice with mixfix syntac *)
(* ------------------------------------------------------------------------ *)
-val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
+bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
(* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *)
-val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
+bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
(* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
@@ -93,7 +93,7 @@
]);
-val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
+bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *)
(* ------------------------------------------------------------------------ *)
@@ -125,7 +125,7 @@
]);
-val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
+bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
(* is_chain(?F) ==> is_chain (%i. ?F i`?x) *)
@@ -210,7 +210,7 @@
(etac (monofun_fapp1 RS ub2ub_monofun) 1)
]);
-val thelub_cfun = (lub_cfun RS thelubI);
+bind_thm ("thelub_cfun", lub_cfun RS thelubI);
(*
is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
--- a/src/HOLCF/Cfun3.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cfun3.ML Fri May 31 19:55:19 1996 +0200
@@ -183,7 +183,7 @@
(* lemma for the cont tactic *)
(* ------------------------------------------------------------------------ *)
-val cont2cont_LAM2 = (allI RSN (2,(allI RS cont2cont_LAM)));
+bind_thm ("cont2cont_LAM2", allI RSN (2,(allI RS cont2cont_LAM)));
(*
[| !!x. cont (?c1.0 x);
!!y. cont (%x. ?c1.0 x y) |] ==> cont (%x. LAM y. ?c1.0 x y)
@@ -343,10 +343,10 @@
]);
-val cont_Istrictify1 = (contlub_Istrictify1 RS
+bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS
(monofun_Istrictify1 RS monocontlub2cont));
-val cont_Istrictify2 = (contlub_Istrictify2 RS
+bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS
(monofun_Istrictify2 RS monocontlub2cont));
--- a/src/HOLCF/Cont.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cont.ML Fri May 31 19:55:19 1996 +0200
@@ -578,7 +578,7 @@
]);
-val cont2cont_app2 = (allI RSN (2,cont2cont_app));
+bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
(* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
(* cont (%x. ?ft x (?tt x)) *)
--- a/src/HOLCF/Cprod2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cprod2.ML Fri May 31 19:55:19 1996 +0200
@@ -160,7 +160,7 @@
(etac (monofun_snd RS ub2ub_monofun) 1)
]);
-val thelub_cprod = (lub_cprod RS thelubI);
+bind_thm ("thelub_cprod", lub_cprod RS thelubI);
(*
"is_chain ?S1 ==>
lub (range ?S1) =
--- a/src/HOLCF/Cprod3.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cprod3.ML Fri May 31 19:55:19 1996 +0200
@@ -283,7 +283,7 @@
(atac 1)
]);
-val thelub_cprod2 = (lub_cprod2 RS thelubI);
+bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
(*
is_chain ?S1 ==>
lub (range ?S1) =
--- a/src/HOLCF/Fix.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Fix.ML Fri May 31 19:55:19 1996 +0200
@@ -587,7 +587,7 @@
]);
-val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
+bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
(* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
@@ -828,7 +828,7 @@
(etac spec 1)
]);
-val adm_all2 = (allI RS adm_all);
+bind_thm ("adm_all2", allI RS adm_all);
qed_goal "adm_subst" Fix.thy
"[|cont t; adm P|] ==> adm(%x. P (t x))"
--- a/src/HOLCF/Fun2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Fun2.ML Fri May 31 19:55:19 1996 +0200
@@ -92,7 +92,7 @@
(etac ub2ub_fun 1)
]);
-val thelub_fun = (lub_fun RS thelubI);
+bind_thm ("thelub_fun", lub_fun RS thelubI);
(* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
qed_goal "cpo_fun" Fun2.thy
--- a/src/HOLCF/Lift2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Lift2.ML Fri May 31 19:55:19 1996 +0200
@@ -154,13 +154,13 @@
(rtac minimal_lift 1)
]);
-val thelub_lift1a = lub_lift1a RS thelubI;
+bind_thm ("thelub_lift1a", lub_lift1a RS thelubI);
(*
[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i))))
*)
-val thelub_lift1b = lub_lift1b RS thelubI;
+bind_thm ("thelub_lift1b", lub_lift1b RS thelubI);
(*
[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
lub (range ?Y1) = UU_lift
--- a/src/HOLCF/Pcpo.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Pcpo.ML Fri May 31 19:55:19 1996 +0200
@@ -27,10 +27,10 @@
(* ------------------------------------------------------------------------ *)
-val is_ub_thelub = (cpo RS lubI RS is_ub_lub);
+bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
(* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *)
-val is_lub_thelub = (cpo RS lubI RS is_lub_lub);
+bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
--- a/src/HOLCF/Porder.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Porder.ML Fri May 31 19:55:19 1996 +0200
@@ -216,10 +216,10 @@
(etac spec 1)
]);
-val is_ub_lub = (is_lubE RS conjunct1 RS ub_rangeE RS spec);
+bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
-val is_lub_lub = (is_lubE RS conjunct2 RS spec RS mp);
+bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *)
(* ------------------------------------------------------------------------ *)
@@ -276,7 +276,7 @@
(* lub(?M) = UU_void *)
(* ------------------------------------------------------------------------ *)
-val thelub_void = (lub_void RS thelubI);
+bind_thm ("thelub_void", lub_void RS thelubI);
(* ------------------------------------------------------------------------ *)
(* void is a cpo wrt. countable chains *)
--- a/src/HOLCF/ROOT.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/ROOT.ML Fri May 31 19:55:19 1996 +0200
@@ -11,6 +11,8 @@
init_thy_reader();
(* start 8bit 1 *)
+val banner =
+ "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
(* end 8bit 1 *)
writeln banner;
--- a/src/HOLCF/Sprod2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Sprod2.ML Fri May 31 19:55:19 1996 +0200
@@ -42,7 +42,7 @@
(etac (inst_sprod_po RS subst) 1)
]);
-val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
+bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
(* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
qed_goal "less_sprod4c" Sprod2.thy
@@ -252,7 +252,7 @@
(etac (monofun_Issnd RS ub2ub_monofun) 1)
]);
-val thelub_sprod = (lub_sprod RS thelubI);
+bind_thm ("thelub_sprod", lub_sprod RS thelubI);
qed_goal "cpo_sprod" Sprod2.thy
--- a/src/HOLCF/Sprod3.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Sprod3.ML Fri May 31 19:55:19 1996 +0200
@@ -612,7 +612,7 @@
]);
-val thelub_sprod2 = (lub_sprod2 RS thelubI);
+bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
(*
"is_chain ?S1 ==>
lub (range ?S1) =
--- a/src/HOLCF/Ssum2.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Ssum2.ML Fri May 31 19:55:19 1996 +0200
@@ -390,14 +390,14 @@
]);
-val thelub_ssum1a = lub_ssum1a RS thelubI;
+bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
(*
[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
lub (range ?Y1) = Isinl
(lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
*)
-val thelub_ssum1b = lub_ssum1b RS thelubI;
+bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI);
(*
[| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
lub (range ?Y1) = Isinr