introduced forgotten bind_thm calls
authoroheimb
Fri May 31 19:55:19 1996 +0200 (1996-05-31)
changeset 17791155c06fa956
parent 1778 6c942cf3bf68
child 1780 e6656a445a33
introduced forgotten bind_thm calls
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod3.ML
src/HOLCF/Fix.ML
src/HOLCF/Fun2.ML
src/HOLCF/Lift2.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder.ML
src/HOLCF/ROOT.ML
src/HOLCF/Sprod2.ML
src/HOLCF/Sprod3.ML
src/HOLCF/Ssum2.ML
     1.1 --- a/src/HOLCF/Cfun2.ML	Fri May 31 19:47:23 1996 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Fri May 31 19:55:19 1996 +0200
     1.3 @@ -48,11 +48,11 @@
     1.4          (rtac Rep_Cfun 1)
     1.5          ]);
     1.6  
     1.7 -val monofun_fapp2 = cont_fapp2 RS cont2mono;
     1.8 +bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
     1.9  (* monofun(fapp(?fo1)) *)
    1.10  
    1.11  
    1.12 -val contlub_fapp2 = cont_fapp2 RS cont2contlub;
    1.13 +bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
    1.14  (* contlub(fapp(?fo1)) *)
    1.15  
    1.16  (* ------------------------------------------------------------------------ *)
    1.17 @@ -60,10 +60,10 @@
    1.18  (* looks nice with mixfix syntac                                            *)
    1.19  (* ------------------------------------------------------------------------ *)
    1.20  
    1.21 -val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
    1.22 +bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
    1.23  (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    1.24   
    1.25 -val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
    1.26 +bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    1.27  (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    1.28  
    1.29  
    1.30 @@ -93,7 +93,7 @@
    1.31          ]);
    1.32  
    1.33  
    1.34 -val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    1.35 +bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
    1.36  (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
    1.37  
    1.38  (* ------------------------------------------------------------------------ *)
    1.39 @@ -125,7 +125,7 @@
    1.40          ]);
    1.41  
    1.42  
    1.43 -val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
    1.44 +bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
    1.45  (* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
    1.46  
    1.47  
    1.48 @@ -210,7 +210,7 @@
    1.49          (etac (monofun_fapp1 RS ub2ub_monofun) 1)
    1.50          ]);
    1.51  
    1.52 -val thelub_cfun = (lub_cfun RS thelubI);
    1.53 +bind_thm ("thelub_cfun", lub_cfun RS thelubI);
    1.54  (* 
    1.55  is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
    1.56  *)
     2.1 --- a/src/HOLCF/Cfun3.ML	Fri May 31 19:47:23 1996 +0200
     2.2 +++ b/src/HOLCF/Cfun3.ML	Fri May 31 19:55:19 1996 +0200
     2.3 @@ -183,7 +183,7 @@
     2.4  (* lemma for the cont tactic                                               *)
     2.5  (* ------------------------------------------------------------------------ *)
     2.6  
     2.7 -val cont2cont_LAM2 = (allI RSN (2,(allI RS cont2cont_LAM)));
     2.8 +bind_thm ("cont2cont_LAM2", allI RSN (2,(allI RS cont2cont_LAM)));
     2.9  (*
    2.10  [| !!x. cont (?c1.0 x);
    2.11      !!y. cont (%x. ?c1.0 x y) |] ==> cont (%x. LAM y. ?c1.0 x y)
    2.12 @@ -343,10 +343,10 @@
    2.13          ]);
    2.14  
    2.15  
    2.16 -val cont_Istrictify1 = (contlub_Istrictify1 RS 
    2.17 +bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS 
    2.18          (monofun_Istrictify1 RS monocontlub2cont)); 
    2.19  
    2.20 -val cont_Istrictify2 = (contlub_Istrictify2 RS 
    2.21 +bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS 
    2.22          (monofun_Istrictify2 RS monocontlub2cont)); 
    2.23  
    2.24  
     3.1 --- a/src/HOLCF/Cont.ML	Fri May 31 19:47:23 1996 +0200
     3.2 +++ b/src/HOLCF/Cont.ML	Fri May 31 19:55:19 1996 +0200
     3.3 @@ -578,7 +578,7 @@
     3.4          ]);
     3.5  
     3.6  
     3.7 -val cont2cont_app2 = (allI RSN (2,cont2cont_app));
     3.8 +bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
     3.9  (*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
    3.10  (*        cont (%x. ?ft x (?tt x))                    *)
    3.11  
     4.1 --- a/src/HOLCF/Cprod2.ML	Fri May 31 19:47:23 1996 +0200
     4.2 +++ b/src/HOLCF/Cprod2.ML	Fri May 31 19:55:19 1996 +0200
     4.3 @@ -160,7 +160,7 @@
     4.4          (etac (monofun_snd RS ub2ub_monofun) 1)
     4.5          ]);
     4.6  
     4.7 -val thelub_cprod = (lub_cprod RS thelubI);
     4.8 +bind_thm ("thelub_cprod", lub_cprod RS thelubI);
     4.9  (*
    4.10  "is_chain ?S1 ==>
    4.11   lub (range ?S1) =
     5.1 --- a/src/HOLCF/Cprod3.ML	Fri May 31 19:47:23 1996 +0200
     5.2 +++ b/src/HOLCF/Cprod3.ML	Fri May 31 19:55:19 1996 +0200
     5.3 @@ -283,7 +283,7 @@
     5.4          (atac 1)
     5.5          ]);
     5.6  
     5.7 -val thelub_cprod2 = (lub_cprod2 RS thelubI);
     5.8 +bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
     5.9  (*
    5.10  is_chain ?S1 ==>
    5.11   lub (range ?S1) =
     6.1 --- a/src/HOLCF/Fix.ML	Fri May 31 19:47:23 1996 +0200
     6.2 +++ b/src/HOLCF/Fix.ML	Fri May 31 19:55:19 1996 +0200
     6.3 @@ -587,7 +587,7 @@
     6.4          ]);
     6.5  
     6.6  
     6.7 -val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
     6.8 +bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
     6.9  (* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
    6.10  
    6.11  qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
    6.12 @@ -828,7 +828,7 @@
    6.13          (etac spec 1)
    6.14          ]);
    6.15  
    6.16 -val adm_all2 = (allI RS adm_all);
    6.17 +bind_thm ("adm_all2", allI RS adm_all);
    6.18  
    6.19  qed_goal "adm_subst"  Fix.thy  
    6.20          "[|cont t; adm P|] ==> adm(%x. P (t x))"
     7.1 --- a/src/HOLCF/Fun2.ML	Fri May 31 19:47:23 1996 +0200
     7.2 +++ b/src/HOLCF/Fun2.ML	Fri May 31 19:55:19 1996 +0200
     7.3 @@ -92,7 +92,7 @@
     7.4          (etac ub2ub_fun 1)
     7.5          ]);
     7.6  
     7.7 -val thelub_fun = (lub_fun RS thelubI);
     7.8 +bind_thm ("thelub_fun", lub_fun RS thelubI);
     7.9  (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
    7.10  
    7.11  qed_goal "cpo_fun"  Fun2.thy
     8.1 --- a/src/HOLCF/Lift2.ML	Fri May 31 19:47:23 1996 +0200
     8.2 +++ b/src/HOLCF/Lift2.ML	Fri May 31 19:55:19 1996 +0200
     8.3 @@ -154,13 +154,13 @@
     8.4          (rtac minimal_lift 1)
     8.5          ]);
     8.6  
     8.7 -val thelub_lift1a = lub_lift1a RS thelubI;
     8.8 +bind_thm ("thelub_lift1a", lub_lift1a RS thelubI);
     8.9  (*
    8.10  [| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==>
    8.11   lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i))))
    8.12  *)
    8.13  
    8.14 -val thelub_lift1b = lub_lift1b RS thelubI;
    8.15 +bind_thm ("thelub_lift1b", lub_lift1b RS thelubI);
    8.16  (*
    8.17  [| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
    8.18   lub (range ?Y1) = UU_lift
     9.1 --- a/src/HOLCF/Pcpo.ML	Fri May 31 19:47:23 1996 +0200
     9.2 +++ b/src/HOLCF/Pcpo.ML	Fri May 31 19:55:19 1996 +0200
     9.3 @@ -27,10 +27,10 @@
     9.4  (* ------------------------------------------------------------------------ *)
     9.5  
     9.6  
     9.7 -val is_ub_thelub = (cpo RS lubI RS is_ub_lub);
     9.8 +bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
     9.9  (* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
    9.10  
    9.11 -val is_lub_thelub = (cpo RS lubI RS is_lub_lub);
    9.12 +bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
    9.13  (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
    9.14  
    9.15  
    10.1 --- a/src/HOLCF/Porder.ML	Fri May 31 19:47:23 1996 +0200
    10.2 +++ b/src/HOLCF/Porder.ML	Fri May 31 19:55:19 1996 +0200
    10.3 @@ -216,10 +216,10 @@
    10.4          (etac spec 1)
    10.5          ]);
    10.6  
    10.7 -val is_ub_lub = (is_lubE RS conjunct1 RS ub_rangeE RS spec);
    10.8 +bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
    10.9  (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
   10.10  
   10.11 -val is_lub_lub = (is_lubE RS conjunct2 RS spec RS mp);
   10.12 +bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
   10.13  (* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
   10.14  
   10.15  (* ------------------------------------------------------------------------ *)
   10.16 @@ -276,7 +276,7 @@
   10.17  (* lub(?M) = UU_void                                                        *)
   10.18  (* ------------------------------------------------------------------------ *)
   10.19  
   10.20 -val thelub_void = (lub_void RS thelubI);
   10.21 +bind_thm ("thelub_void", lub_void RS thelubI);
   10.22  
   10.23  (* ------------------------------------------------------------------------ *)
   10.24  (* void is a cpo wrt. countable chains                                      *)
    11.1 --- a/src/HOLCF/ROOT.ML	Fri May 31 19:47:23 1996 +0200
    11.2 +++ b/src/HOLCF/ROOT.ML	Fri May 31 19:55:19 1996 +0200
    11.3 @@ -11,6 +11,8 @@
    11.4  init_thy_reader();
    11.5  
    11.6  (* start 8bit 1 *)
    11.7 +val banner = 
    11.8 +	"HOLCF with sections axioms,ops,domain,generated and 8bit characters";
    11.9  (* end 8bit 1 *)
   11.10  
   11.11  writeln banner;
    12.1 --- a/src/HOLCF/Sprod2.ML	Fri May 31 19:47:23 1996 +0200
    12.2 +++ b/src/HOLCF/Sprod2.ML	Fri May 31 19:55:19 1996 +0200
    12.3 @@ -42,7 +42,7 @@
    12.4          (etac (inst_sprod_po RS subst) 1)
    12.5          ]);
    12.6  
    12.7 -val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    12.8 +bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
    12.9  (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
   12.10  
   12.11  qed_goal "less_sprod4c" Sprod2.thy
   12.12 @@ -252,7 +252,7 @@
   12.13          (etac (monofun_Issnd RS ub2ub_monofun) 1)
   12.14          ]);
   12.15  
   12.16 -val thelub_sprod = (lub_sprod RS thelubI);
   12.17 +bind_thm ("thelub_sprod", lub_sprod RS thelubI);
   12.18  
   12.19  
   12.20  qed_goal "cpo_sprod" Sprod2.thy 
    13.1 --- a/src/HOLCF/Sprod3.ML	Fri May 31 19:47:23 1996 +0200
    13.2 +++ b/src/HOLCF/Sprod3.ML	Fri May 31 19:55:19 1996 +0200
    13.3 @@ -612,7 +612,7 @@
    13.4          ]);
    13.5  
    13.6  
    13.7 -val thelub_sprod2 = (lub_sprod2 RS thelubI);
    13.8 +bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
    13.9  (*
   13.10   "is_chain ?S1 ==>
   13.11   lub (range ?S1) =
    14.1 --- a/src/HOLCF/Ssum2.ML	Fri May 31 19:47:23 1996 +0200
    14.2 +++ b/src/HOLCF/Ssum2.ML	Fri May 31 19:55:19 1996 +0200
    14.3 @@ -390,14 +390,14 @@
    14.4          ]);
    14.5  
    14.6  
    14.7 -val thelub_ssum1a = lub_ssum1a RS thelubI;
    14.8 +bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI);
    14.9  (*
   14.10  [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
   14.11   lub (range ?Y1) = Isinl
   14.12   (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
   14.13  *)
   14.14  
   14.15 -val thelub_ssum1b = lub_ssum1b RS thelubI;
   14.16 +bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI);
   14.17  (*
   14.18  [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
   14.19   lub (range ?Y1) = Isinr