# HG changeset patch
# User oheimb
# Date 833565319 -7200
# Node ID 1155c06fa9567c20cd9facabaaf401e161b21578
# Parent  6c942cf3bf68ddc2954c022ea349c752d105d33d
introduced forgotten bind_thm calls

diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cfun2.ML
--- 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)))
 *)
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cfun3.ML
--- 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)); 
 
 
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cont.ML
--- 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))                    *)
 
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cprod2.ML
--- 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) =
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cprod3.ML
--- 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) =
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Fix.ML
--- 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))"
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Fun2.ML
--- 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
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Lift2.ML
--- 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
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Pcpo.ML
--- 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        *)
 
 
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Porder.ML
--- 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                                      *)
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/ROOT.ML
--- 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;
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Sprod2.ML
--- 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 
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Sprod3.ML
--- 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) =
diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Ssum2.ML
--- 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