src/HOL/Univ.ML
changeset 9108 9fff97d29837
parent 8790 c4aaa5936e0c
child 9162 647d554a65ae
     1.1 --- a/src/HOL/Univ.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Univ.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  by (etac Abs_Node_inverse 1);
     1.5  qed "inj_on_Abs_Node";
     1.6  
     1.7 -val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
     1.8 +bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
     1.9  
    1.10  
    1.11  (*** Introduction rules for Node ***)
    1.12 @@ -98,7 +98,7 @@
    1.13  Goalw [Atom_def] "inj(Atom)";
    1.14  by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
    1.15  qed "inj_Atom";
    1.16 -val Atom_inject = inj_Atom RS injD;
    1.17 +bind_thm ("Atom_inject", inj_Atom RS injD);
    1.18  
    1.19  Goal "(Atom(a)=Atom(b)) = (a=b)";
    1.20  by (blast_tac (claset() addSDs [Atom_inject]) 1);
    1.21 @@ -118,7 +118,7 @@
    1.22  by (etac (Atom_inject RS Inr_inject) 1);
    1.23  qed "inj_Numb";
    1.24  
    1.25 -val Numb_inject = inj_Numb RS injD;
    1.26 +bind_thm ("Numb_inject", inj_Numb RS injD);
    1.27  AddSDs [Numb_inject];
    1.28  
    1.29  (** Injectiveness of Push_Node **)
    1.30 @@ -586,7 +586,7 @@
    1.31  by (Blast_tac 1);
    1.32  qed "dprod_Sigma";
    1.33  
    1.34 -val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
    1.35 +bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
    1.36  
    1.37  (*Dependent version*)
    1.38  Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
    1.39 @@ -599,7 +599,7 @@
    1.40  by (Blast_tac 1);
    1.41  qed "dsum_Sigma";
    1.42  
    1.43 -val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
    1.44 +bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
    1.45  
    1.46  
    1.47  (*** Domain ***)