src/HOL/Real/PNat.ML
changeset 9108 9fff97d29837
parent 9043 ca761fe227d8
child 9422 4b6bc2b347e5
     1.1 --- a/src/HOL/Real/PNat.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Real/PNat.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
     1.5  qed "pnat_fun_mono";
     1.6  
     1.7 -val pnat_unfold = pnat_fun_mono RS (pnat_def RS def_lfp_Tarski);
     1.8 +bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
     1.9  
    1.10  Goal "1 : pnat";
    1.11  by (stac pnat_unfold 1);
    1.12 @@ -144,7 +144,7 @@
    1.13  AddIffs [pSuc_not_one,one_not_pSuc];
    1.14  
    1.15  bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
    1.16 -val one_neq_pSuc = sym RS pSuc_neq_one;
    1.17 +bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
    1.18  
    1.19  (** Injectiveness of pSuc **)
    1.20  
    1.21 @@ -156,7 +156,7 @@
    1.22  by (etac (inj_Rep_pnat RS injD) 1);
    1.23  qed "inj_pSuc"; 
    1.24  
    1.25 -val pSuc_inject = inj_pSuc RS injD;
    1.26 +bind_thm ("pSuc_inject", inj_pSuc RS injD);
    1.27  
    1.28  Goal "(pSuc(m)=pSuc(n)) = (m=n)";
    1.29  by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); 
    1.30 @@ -209,7 +209,7 @@
    1.31  qed "pnat_add_left_commute";
    1.32  
    1.33  (*Addition is an AC-operator*)
    1.34 -val pnat_add_ac = [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute];
    1.35 +bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
    1.36  
    1.37  Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
    1.38  by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
    1.39 @@ -306,7 +306,7 @@
    1.40  by (assume_tac 1);
    1.41  qed "pnat_leD";
    1.42  
    1.43 -val pnat_leE = make_elim pnat_leD;
    1.44 +bind_thm ("pnat_leE", make_elim pnat_leD);
    1.45  
    1.46  Goal "(~ (x::pnat) < y) = (y <= x)";
    1.47  by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
    1.48 @@ -594,7 +594,7 @@
    1.49  qed "pnat_mult_1_left";
    1.50  
    1.51  (*Multiplication is an AC-operator*)
    1.52 -val pnat_mult_ac = [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute];
    1.53 +bind_thms ("pnat_mult_ac", [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
    1.54  
    1.55  Goal "!!i j k::pnat. i<=j ==> i * k <= j * k";
    1.56  by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,