src/HOL/Sum.ML
changeset 9108 9fff97d29837
parent 7293 959e060f4a2f
child 9311 ab5b24cbaa16
     1.1 --- a/src/HOL/Sum.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -43,8 +43,7 @@
     1.4  AddIffs [Inl_not_Inr, Inr_not_Inl];
     1.5  
     1.6  bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
     1.7 -
     1.8 -val Inr_neq_Inl = sym RS Inl_neq_Inr;
     1.9 +bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr);
    1.10  
    1.11  
    1.12  (** Injectiveness of Inl and Inr **)
    1.13 @@ -65,7 +64,7 @@
    1.14  by (rtac Inl_RepI 1);
    1.15  by (rtac Inl_RepI 1);
    1.16  qed "inj_Inl";
    1.17 -val Inl_inject = inj_Inl RS injD;
    1.18 +bind_thm ("Inl_inject", inj_Inl RS injD);
    1.19  
    1.20  Goalw [Inr_def] "inj(Inr)";
    1.21  by (rtac injI 1);
    1.22 @@ -73,7 +72,7 @@
    1.23  by (rtac Inr_RepI 1);
    1.24  by (rtac Inr_RepI 1);
    1.25  qed "inj_Inr";
    1.26 -val Inr_inject = inj_Inr RS injD;
    1.27 +bind_thm ("Inr_inject", inj_Inr RS injD);
    1.28  
    1.29  Goal "(Inl(x)=Inl(y)) = (x=y)";
    1.30  by (blast_tac (claset() addSDs [Inl_inject]) 1);
    1.31 @@ -138,7 +137,7 @@
    1.32  by (Blast_tac 1);
    1.33  qed "Part_eqI";
    1.34  
    1.35 -val PartI = refl RSN (2,Part_eqI);
    1.36 +bind_thm ("PartI", refl RSN (2,Part_eqI));
    1.37  
    1.38  val major::prems = Goalw [Part_def]
    1.39      "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \