src/HOL/Real/PNat.ML

 
 Goal "mono(%X. {1} Un (Suc``X))";
 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
 qed "pnat_fun_mono";
 
-val pnat_unfold = pnat_fun_mono RS (pnat_def RS def_lfp_Tarski);
+bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
 
 Goal "1 : pnat";
 by (stac pnat_unfold 1);
 by (rtac (singletonI RS UnI1) 1);
 qed "one_RepI";

 bind_thm ("one_not_pSuc", pSuc_not_one RS not_sym);
 
 AddIffs [pSuc_not_one,one_not_pSuc];
 
 bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
-val one_neq_pSuc = sym RS pSuc_neq_one;
+bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
 
 (** Injectiveness of pSuc **)
 
 Goalw [pnat_Suc_def] "inj(pSuc)";
 by (rtac injI 1);

 by (REPEAT (resolve_tac [Rep_pnat, pnat_Suc_RepI] 1));
 by (dtac (inj_Suc RS injD) 1);
 by (etac (inj_Rep_pnat RS injD) 1);
 qed "inj_pSuc"; 
 
-val pSuc_inject = inj_pSuc RS injD;
+bind_thm ("pSuc_inject", inj_pSuc RS injD);
 
 Goal "(pSuc(m)=pSuc(n)) = (m=n)";
 by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); 
 qed "pSuc_pSuc_eq";
 

 by (simp_tac (simpset() addsimps [sum_Rep_pnat RS 
           Abs_pnat_inverse,add_left_commute]) 1);
 qed "pnat_add_left_commute";
 
 (*Addition is an AC-operator*)
-val pnat_add_ac = [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute];
+bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
 
 Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
 by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
      inj_Rep_pnat RS injD],simpset() addsimps [sum_Rep_pnat]));
 qed "pnat_add_left_cancel";

 
 Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
 by (assume_tac 1);
 qed "pnat_leD";
 
-val pnat_leE = make_elim pnat_leD;
+bind_thm ("pnat_leE", make_elim pnat_leD);
 
 Goal "(~ (x::pnat) < y) = (y <= x)";
 by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
 qed "pnat_not_less_iff_le";
 

 by (full_simp_tac (simpset() addsimps [pnat_mult_1,
                    pnat_mult_commute]) 1);
 qed "pnat_mult_1_left";
 
 (*Multiplication is an AC-operator*)
-val pnat_mult_ac = [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute];
+bind_thms ("pnat_mult_ac", [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
 
 Goal "!!i j k::pnat. i<=j ==> i * k <= j * k";
 by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
                      mult_Rep_pnat_mult RS sym,mult_le_mono1]) 1);
 qed "pnat_mult_le_mono1";