bind_thm(s);
authorwenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 91089fff97d29837
parent 9107 67202a50ee6d
child 9109 0085c32a533b
bind_thm(s);
src/HOL/Datatype.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/IntDef.ML
src/HOL/Integ/IntDiv.ML
src/HOL/Integ/NatBin.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/RealBin.ML
src/HOL/Real/RealDef.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/WF_Rel.ML
     1.1 --- a/src/HOL/Datatype.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Datatype.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  (*compatibility*)
     1.6  val [sum_case_Inl, sum_case_Inr] = sum.cases;
     1.7 +bind_thm ("sum_case_Inl", sum_case_Inl);
     1.8 +bind_thm ("sum_case_Inr", sum_case_Inr);
     1.9  
    1.10  Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.11  by (EVERY1 [res_inst_tac [("s","s")] sumE, 
     2.1 --- a/src/HOL/Divides.ML	Thu Jun 22 11:37:13 2000 +0200
     2.2 +++ b/src/HOL/Divides.ML	Thu Jun 22 23:04:34 2000 +0200
     2.3 @@ -9,8 +9,8 @@
     2.4  
     2.5  (** Less-then properties **)
     2.6  
     2.7 -val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
     2.8 -                    def_wfrec RS trans;
     2.9 +bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    2.10 +                    def_wfrec RS trans);
    2.11  
    2.12  Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
    2.13  \                           (%f j. if j<n | n=0 then j else f (j-n))";
     3.1 --- a/src/HOL/Finite.ML	Thu Jun 22 11:37:13 2000 +0200
     3.2 +++ b/src/HOL/Finite.ML	Thu Jun 22 23:04:34 2000 +0200
     3.3 @@ -245,8 +245,8 @@
     3.4  
     3.5  section "Finite cardinality -- 'card'";
     3.6  
     3.7 -val cardR_emptyE = cardR.mk_cases "({},n) : cardR";
     3.8 -val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR";
     3.9 +bind_thm ("cardR_emptyE", cardR.mk_cases "({},n) : cardR");
    3.10 +bind_thm ("cardR_insertE", cardR.mk_cases "(insert a A,n) : cardR");
    3.11  
    3.12  AddSEs [cardR_emptyE];
    3.13  AddSIs cardR.intrs;
    3.14 @@ -491,7 +491,7 @@
    3.15  
    3.16  (*** foldSet ***)
    3.17  
    3.18 -val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e";
    3.19 +bind_thm ("empty_foldSetE", foldSet.mk_cases "({}, x) : foldSet f e");
    3.20  
    3.21  AddSEs [empty_foldSetE];
    3.22  AddIs foldSet.intrs;
     4.1 --- a/src/HOL/Fun.ML	Thu Jun 22 11:37:13 2000 +0200
     4.2 +++ b/src/HOL/Fun.ML	Thu Jun 22 23:04:34 2000 +0200
     4.3 @@ -151,7 +151,7 @@
     4.4      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
     4.5  by (blast_tac (claset() addIs prems) 1);
     4.6  qed "inj_onI";
     4.7 -val injI = inj_onI;                  (*for compatibility*)
     4.8 +bind_thm ("injI", inj_onI);                  (*for compatibility*)
     4.9  
    4.10  val [major] = Goal 
    4.11      "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
    4.12 @@ -159,7 +159,7 @@
    4.13  by (etac (apply_inverse RS trans) 1);
    4.14  by (REPEAT (eresolve_tac [asm_rl,major] 1));
    4.15  qed "inj_on_inverseI";
    4.16 -val inj_inverseI = inj_on_inverseI;   (*for compatibility*)
    4.17 +bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
    4.18  
    4.19  Goal "(inj f) = (inv f o f = id)";
    4.20  by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
    4.21 @@ -483,7 +483,7 @@
    4.22  Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
    4.23  by (rtac ext 1);
    4.24  by Auto_tac;
    4.25 -val Pi_extensionality = ballI RSN (3, result());
    4.26 +bind_thm ("Pi_extensionality", ballI RSN (3, result()));
    4.27  
    4.28  
    4.29  (*** compose ***)
     5.1 --- a/src/HOL/Integ/Bin.ML	Thu Jun 22 11:37:13 2000 +0200
     5.2 +++ b/src/HOL/Integ/Bin.ML	Thu Jun 22 23:04:34 2000 +0200
     5.3 @@ -128,7 +128,7 @@
     5.4  qed "number_of_minus";
     5.5  
     5.6   
     5.7 -val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred];
     5.8 +bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]);
     5.9  
    5.10  (*This proof is complicated by the mutual recursion*)
    5.11  Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
    5.12 @@ -147,7 +147,7 @@
    5.13  by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
    5.14  qed "diff_number_of_eq";
    5.15  
    5.16 -val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add];
    5.17 +bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]);
    5.18  
    5.19  Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
    5.20  by (induct_tac "v" 1);
    5.21 @@ -407,10 +407,9 @@
    5.22  (*Simplification of arithmetic operations on integer constants.
    5.23    Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
    5.24  
    5.25 -val NCons_simps = [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, 
    5.26 -		   NCons_BIT];
    5.27 +bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
    5.28  
    5.29 -val bin_arith_extra_simps =
    5.30 +bind_thms ("bin_arith_extra_simps",
    5.31      [number_of_add RS sym,
    5.32       number_of_minus RS sym,
    5.33       number_of_mult RS sym,
    5.34 @@ -420,24 +419,24 @@
    5.35       bin_add_Pls_right, bin_add_Min_right,
    5.36       bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
    5.37       diff_number_of_eq, 
    5.38 -     bin_mult_1, bin_mult_0] @ NCons_simps;
    5.39 +     bin_mult_1, bin_mult_0] @ NCons_simps);
    5.40  
    5.41  (*For making a minimal simpset, one must include these default simprules
    5.42    of thy.  Also include simp_thms, or at least (~False)=True*)
    5.43 -val bin_arith_simps =
    5.44 +bind_thms ("bin_arith_simps",
    5.45      [bin_pred_Pls, bin_pred_Min,
    5.46       bin_succ_Pls, bin_succ_Min,
    5.47       bin_add_Pls, bin_add_Min,
    5.48       bin_minus_Pls, bin_minus_Min,
    5.49 -     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps;
    5.50 +     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
    5.51  
    5.52  (*Simplification of relational operations*)
    5.53 -val bin_rel_simps =
    5.54 +bind_thms ("bin_rel_simps",
    5.55      [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
    5.56       iszero_number_of_0, iszero_number_of_1,
    5.57       less_number_of_eq_neg,
    5.58       not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
    5.59 -     le_number_of_eq_not_less];
    5.60 +     le_number_of_eq_not_less]);
    5.61  
    5.62  Addsimps bin_arith_extra_simps;
    5.63  Addsimps bin_rel_simps;
     6.1 --- a/src/HOL/Integ/IntDef.ML	Thu Jun 22 11:37:13 2000 +0200
     6.2 +++ b/src/HOL/Integ/IntDef.ML	Thu Jun 22 23:04:34 2000 +0200
     6.3 @@ -61,7 +61,7 @@
     6.4                         addSEs [sym, integ_trans_lemma]) 1);
     6.5  qed "equiv_intrel";
     6.6  
     6.7 -val equiv_intrel_iff = [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
     6.8 +bind_thm ("equiv_intrel_iff", [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
     6.9  
    6.10  Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
    6.11  by (Fast_tac 1);
    6.12 @@ -586,11 +586,11 @@
    6.13  (*This list of rewrites simplifies (in)equalities by bringing subtractions
    6.14    to the top and then moving negative terms to the other side.  
    6.15    Use with zadd_ac*)
    6.16 -val zcompare_rls = 
    6.17 +bind_thms ("zcompare_rls",
    6.18      [symmetric zdiff_def,
    6.19       zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
    6.20       zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 
    6.21 -     zdiff_eq_eq, eq_zdiff_eq];
    6.22 +     zdiff_eq_eq, eq_zdiff_eq]);
    6.23  
    6.24  
    6.25  (** Cancellation laws **)
     7.1 --- a/src/HOL/Integ/IntDiv.ML	Thu Jun 22 11:37:13 2000 +0200
     7.2 +++ b/src/HOL/Integ/IntDiv.ML	Thu Jun 22 23:04:34 2000 +0200
     7.3 @@ -108,7 +108,7 @@
     7.4  by (Asm_simp_tac 1);
     7.5  qed "posDivAlg_eqn";
     7.6  
     7.7 -val posDivAlg_induct = lemma RS posDivAlg.induct;
     7.8 +bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct);
     7.9  
    7.10  
    7.11  (*Correctness of posDivAlg: it computes quotients correctly*)
    7.12 @@ -146,7 +146,7 @@
    7.13  by (Asm_simp_tac 1);
    7.14  qed "negDivAlg_eqn";
    7.15  
    7.16 -val negDivAlg_induct = lemma RS negDivAlg.induct;
    7.17 +bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct);
    7.18  
    7.19  
    7.20  (*Correctness of negDivAlg: it computes quotients correctly
     8.1 --- a/src/HOL/Integ/NatBin.ML	Thu Jun 22 11:37:13 2000 +0200
     8.2 +++ b/src/HOL/Integ/NatBin.ML	Thu Jun 22 23:04:34 2000 +0200
     8.3 @@ -345,13 +345,13 @@
     8.4  Addsimps [inst "n" "number_of ?v" diff_less'];
     8.5  
     8.6  (*various theorems that aren't in the default simpset*)
     8.7 -val add_is_one' = rename_numerals thy add_is_1;
     8.8 -val one_is_add' = rename_numerals thy one_is_add;
     8.9 -val zero_induct' = rename_numerals thy zero_induct;
    8.10 -val diff_self_eq_0' = rename_numerals thy diff_self_eq_0;
    8.11 -val mult_eq_self_implies_10' = rename_numerals thy mult_eq_self_implies_10;
    8.12 -val le_pred_eq' = rename_numerals thy le_pred_eq;
    8.13 -val less_pred_eq' = rename_numerals thy less_pred_eq;
    8.14 +bind_thm ("add_is_one'", rename_numerals thy add_is_1);
    8.15 +bind_thm ("one_is_add'", rename_numerals thy one_is_add);
    8.16 +bind_thm ("zero_induct'", rename_numerals thy zero_induct);
    8.17 +bind_thm ("diff_self_eq_0'", rename_numerals thy diff_self_eq_0);
    8.18 +bind_thm ("mult_eq_self_implies_10'", rename_numerals thy mult_eq_self_implies_10);
    8.19 +bind_thm ("le_pred_eq'", rename_numerals thy le_pred_eq);
    8.20 +bind_thm ("less_pred_eq'", rename_numerals thy less_pred_eq);
    8.21  
    8.22  (** Divides **)
    8.23  
    8.24 @@ -361,10 +361,10 @@
    8.25  	  [dvd_1_left, dvd_0_right]);
    8.26  
    8.27  (*useful?*)
    8.28 -val mod_self' = rename_numerals thy mod_self;
    8.29 -val div_self' = rename_numerals thy div_self;
    8.30 -val div_less' = rename_numerals thy div_less;
    8.31 -val mod_mult_self_is_zero' = rename_numerals thy mod_mult_self_is_0;
    8.32 +bind_thm ("mod_self'", rename_numerals thy mod_self);
    8.33 +bind_thm ("div_self'", rename_numerals thy div_self);
    8.34 +bind_thm ("div_less'", rename_numerals thy div_less);
    8.35 +bind_thm ("mod_mult_self_is_zero'", rename_numerals thy mod_mult_self_is_0);
    8.36  
    8.37  (** Power **)
    8.38  
    8.39 @@ -386,9 +386,9 @@
    8.40  qed "zero_less_power'";
    8.41  Addsimps [zero_less_power'];
    8.42  
    8.43 -val binomial_zero = rename_numerals thy binomial_0;
    8.44 -val binomial_Suc' = rename_numerals thy binomial_Suc;
    8.45 -val binomial_n_n' = rename_numerals thy binomial_n_n;
    8.46 +bind_thm ("binomial_zero", rename_numerals thy binomial_0);
    8.47 +bind_thm ("binomial_Suc'", rename_numerals thy binomial_Suc);
    8.48 +bind_thm ("binomial_n_n'", rename_numerals thy binomial_n_n);
    8.49  
    8.50  (*binomial_0_Suc doesn't work well on numerals*)
    8.51  Addsimps (map (rename_numerals thy) 
     9.1 --- a/src/HOL/List.ML	Thu Jun 22 11:37:13 2000 +0200
     9.2 +++ b/src/HOL/List.ML	Thu Jun 22 23:04:34 2000 +0200
     9.3 @@ -32,7 +32,7 @@
     9.4  by (REPEAT (ares_tac basic_monos 1));
     9.5  qed "lists_mono";
     9.6  
     9.7 -val listsE = lists.mk_cases "x#l : lists A";
     9.8 +bind_thm ("listsE", lists.mk_cases "x#l : lists A");
     9.9  AddSEs [listsE];
    9.10  AddSIs lists.intrs;
    9.11  
    10.1 --- a/src/HOL/Nat.ML	Thu Jun 22 11:37:13 2000 +0200
    10.2 +++ b/src/HOL/Nat.ML	Thu Jun 22 23:04:34 2000 +0200
    10.3 @@ -7,6 +7,8 @@
    10.4  (** conversion rules for nat_rec **)
    10.5  
    10.6  val [nat_rec_0, nat_rec_Suc] = nat.recs;
    10.7 +bind_thm ("nat_rec_0", nat_rec_0);
    10.8 +bind_thm ("nat_rec_Suc", nat_rec_Suc);
    10.9  
   10.10  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
   10.11  val prems = Goal
   10.12 @@ -20,6 +22,8 @@
   10.13  qed "def_nat_rec_Suc";
   10.14  
   10.15  val [nat_case_0, nat_case_Suc] = nat.cases;
   10.16 +bind_thm ("nat_case_0", nat_case_0);
   10.17 +bind_thm ("nat_case_Suc", nat_case_Suc);
   10.18  
   10.19  Goal "n ~= 0 ==> EX m. n = Suc m";
   10.20  by (case_tac "n" 1);
    11.1 --- a/src/HOL/NatDef.ML	Thu Jun 22 11:37:13 2000 +0200
    11.2 +++ b/src/HOL/NatDef.ML	Thu Jun 22 23:04:34 2000 +0200
    11.3 @@ -8,7 +8,7 @@
    11.4  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    11.5  qed "Nat_fun_mono";
    11.6  
    11.7 -val Nat_unfold = Nat_fun_mono RS (Nat_def RS def_lfp_Tarski);
    11.8 +bind_thm ("Nat_unfold", Nat_fun_mono RS (Nat_def RS def_lfp_Tarski));
    11.9  
   11.10  (* Zero is a natural number -- this also justifies the type definition*)
   11.11  Goal "Zero_Rep: Nat";
   11.12 @@ -85,7 +85,7 @@
   11.13  AddIffs [Suc_not_Zero,Zero_not_Suc];
   11.14  
   11.15  bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
   11.16 -val Zero_neq_Suc = sym RS Suc_neq_Zero;
   11.17 +bind_thm ("Zero_neq_Suc", sym RS Suc_neq_Zero);
   11.18  
   11.19  (** Injectiveness of Suc **)
   11.20  
   11.21 @@ -97,7 +97,7 @@
   11.22  by (etac (inj_Rep_Nat RS injD) 1);
   11.23  qed "inj_Suc";
   11.24  
   11.25 -val Suc_inject = inj_Suc RS injD;
   11.26 +bind_thm ("Suc_inject", inj_Suc RS injD);
   11.27  
   11.28  Goal "(Suc(m)=Suc(n)) = (m=n)";
   11.29  by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
   11.30 @@ -339,7 +339,7 @@
   11.31  by (assume_tac 1);
   11.32  qed "leD";
   11.33  
   11.34 -val leE = make_elim leD;
   11.35 +bind_thm ("leE", make_elim leD);
   11.36  
   11.37  Goal "(~n<m) = (m<=(n::nat))";
   11.38  by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
   11.39 @@ -384,7 +384,7 @@
   11.40  qed "less_imp_le";
   11.41  
   11.42  (*For instance, (Suc m < Suc n)  =   (Suc m <= n)  =  (m<n) *)
   11.43 -val le_simps = [less_imp_le, less_Suc_eq_le, Suc_le_eq];
   11.44 +bind_thms ("le_simps", [less_imp_le, less_Suc_eq_le, Suc_le_eq]);
   11.45  
   11.46  
   11.47  (** Equivalence of m<=n and  m<n | m=n **)
   11.48 @@ -461,7 +461,7 @@
   11.49  
   11.50  (*Rewrite (n < Suc m) to (n=m) if  ~ n<m or m<=n hold.
   11.51    Not suitable as default simprules because they often lead to looping*)
   11.52 -val not_less_simps = [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq];
   11.53 +bind_thms ("not_less_simps", [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq]);
   11.54  
   11.55  (** LEAST -- the least number operator **)
   11.56  
    12.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Thu Jun 22 11:37:13 2000 +0200
    12.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Thu Jun 22 23:04:34 2000 +0200
    12.3 @@ -549,6 +549,6 @@
    12.4  by (Blast_tac 1);
    12.5  qed "FreeUltrafilter_ex";
    12.6  
    12.7 -val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
    12.8 +bind_thm ("FreeUltrafilter_Ex", export FreeUltrafilter_ex);
    12.9  
   12.10  Close_locale "UFT";
    13.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Jun 22 11:37:13 2000 +0200
    13.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Jun 22 23:04:34 2000 +0200
    13.3 @@ -210,10 +210,10 @@
    13.4  	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
    13.5  qed "equiv_hyprel";
    13.6  
    13.7 -val equiv_hyprel_iff =
    13.8 +bind_thm ("equiv_hyprel_iff",
    13.9      [TrueI, TrueI] MRS 
   13.10      ([CollectI, CollectI] MRS 
   13.11 -    (equiv_hyprel RS eq_equiv_class_iff));
   13.12 +    (equiv_hyprel RS eq_equiv_class_iff)));
   13.13  
   13.14  Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal";
   13.15  by (Blast_tac 1);
   13.16 @@ -228,7 +228,7 @@
   13.17            hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
   13.18  
   13.19  Addsimps [equiv_hyprel RS eq_equiv_class_iff];
   13.20 -val eq_hyprelD = equiv_hyprel RSN (2,eq_equiv_class);
   13.21 +bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class));
   13.22  
   13.23  Goal "inj(Rep_hypreal)";
   13.24  by (rtac inj_inverseI 1);
   13.25 @@ -400,8 +400,8 @@
   13.26  qed "hypreal_add_left_commute";
   13.27  
   13.28  (* hypreal addition is an AC operator *)
   13.29 -val hypreal_add_ac = [hypreal_add_assoc,hypreal_add_commute,
   13.30 -                      hypreal_add_left_commute];
   13.31 +bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
   13.32 +                      hypreal_add_left_commute]);
   13.33  
   13.34  Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
   13.35  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   13.36 @@ -560,8 +560,8 @@
   13.37             rtac (hypreal_mult_commute RS arg_cong) 1]);
   13.38  
   13.39  (* hypreal multiplication is an AC operator *)
   13.40 -val hypreal_mult_ac = [hypreal_mult_assoc, hypreal_mult_commute, 
   13.41 -                       hypreal_mult_left_commute];
   13.42 +bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, 
   13.43 +                       hypreal_mult_left_commute]);
   13.44  
   13.45  Goalw [hypreal_one_def] "1hr * z = z";
   13.46  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   13.47 @@ -634,7 +634,7 @@
   13.48  by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   13.49  qed "hypreal_add_mult_distrib2";
   13.50  
   13.51 -val hypreal_mult_simps = [hypreal_mult_1, hypreal_mult_1_right];
   13.52 +bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
   13.53  Addsimps hypreal_mult_simps;
   13.54  
   13.55  (*** one and zero are distinct ***)
   13.56 @@ -1002,7 +1002,7 @@
   13.57  by (assume_tac 1);
   13.58  qed "hypreal_leD";
   13.59  
   13.60 -val hypreal_leE = make_elim hypreal_leD;
   13.61 +bind_thm ("hypreal_leE", make_elim hypreal_leD);
   13.62  
   13.63  Goal "(~(w < z)) = (z <= (w::hypreal))";
   13.64  by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
    14.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Thu Jun 22 11:37:13 2000 +0200
    14.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Thu Jun 22 23:04:34 2000 +0200
    14.3 @@ -14,10 +14,10 @@
    14.4  qed "Union_lemma0";
    14.5  
    14.6  (*-- similar to subset_cs in ZF/subset.thy --*)
    14.7 -val thissubset_SIs =
    14.8 +bind_thms ("thissubset_SIs",
    14.9      [subset_refl,Union_least, UN_least, Un_least, 
   14.10       Inter_greatest, Int_greatest,
   14.11 -     Un_upper1, Un_upper2, Int_lower1, Int_lower2];
   14.12 +     Un_upper1, Un_upper2, Int_lower1, Int_lower2]);
   14.13  
   14.14  
   14.15  (*A claset for subset reasoning*)
   14.16 @@ -38,6 +38,9 @@
   14.17  
   14.18  val [TFin_succI, Pow_TFin_UnionI] = TFin.intrs;
   14.19  val TFin_UnionI = PowI RS Pow_TFin_UnionI;
   14.20 +bind_thm ("TFin_succI", TFin_succI);
   14.21 +bind_thm ("Pow_TFin_UnionI", Pow_TFin_UnionI);
   14.22 +bind_thm ("TFin_UnionI", TFin_UnionI);
   14.23  
   14.24  val major::prems = Goal  
   14.25            "[| n : TFin S; \
    15.1 --- a/src/HOL/Real/PNat.ML	Thu Jun 22 11:37:13 2000 +0200
    15.2 +++ b/src/HOL/Real/PNat.ML	Thu Jun 22 23:04:34 2000 +0200
    15.3 @@ -10,7 +10,7 @@
    15.4  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    15.5  qed "pnat_fun_mono";
    15.6  
    15.7 -val pnat_unfold = pnat_fun_mono RS (pnat_def RS def_lfp_Tarski);
    15.8 +bind_thm ("pnat_unfold", pnat_fun_mono RS (pnat_def RS def_lfp_Tarski));
    15.9  
   15.10  Goal "1 : pnat";
   15.11  by (stac pnat_unfold 1);
   15.12 @@ -144,7 +144,7 @@
   15.13  AddIffs [pSuc_not_one,one_not_pSuc];
   15.14  
   15.15  bind_thm ("pSuc_neq_one", (pSuc_not_one RS notE));
   15.16 -val one_neq_pSuc = sym RS pSuc_neq_one;
   15.17 +bind_thm ("one_neq_pSuc", pSuc_neq_one RS pSuc_neq_one);
   15.18  
   15.19  (** Injectiveness of pSuc **)
   15.20  
   15.21 @@ -156,7 +156,7 @@
   15.22  by (etac (inj_Rep_pnat RS injD) 1);
   15.23  qed "inj_pSuc"; 
   15.24  
   15.25 -val pSuc_inject = inj_pSuc RS injD;
   15.26 +bind_thm ("pSuc_inject", inj_pSuc RS injD);
   15.27  
   15.28  Goal "(pSuc(m)=pSuc(n)) = (m=n)";
   15.29  by (EVERY1 [rtac iffI, etac pSuc_inject, etac arg_cong]); 
   15.30 @@ -209,7 +209,7 @@
   15.31  qed "pnat_add_left_commute";
   15.32  
   15.33  (*Addition is an AC-operator*)
   15.34 -val pnat_add_ac = [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute];
   15.35 +bind_thms ("pnat_add_ac", [pnat_add_assoc, pnat_add_commute, pnat_add_left_commute]);
   15.36  
   15.37  Goalw [pnat_add_def] "((x::pnat) + y = x + z) = (y = z)";
   15.38  by (auto_tac (claset() addDs [inj_on_Abs_pnat RS inj_onD,
   15.39 @@ -306,7 +306,7 @@
   15.40  by (assume_tac 1);
   15.41  qed "pnat_leD";
   15.42  
   15.43 -val pnat_leE = make_elim pnat_leD;
   15.44 +bind_thm ("pnat_leE", make_elim pnat_leD);
   15.45  
   15.46  Goal "(~ (x::pnat) < y) = (y <= x)";
   15.47  by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
   15.48 @@ -594,7 +594,7 @@
   15.49  qed "pnat_mult_1_left";
   15.50  
   15.51  (*Multiplication is an AC-operator*)
   15.52 -val pnat_mult_ac = [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute];
   15.53 +bind_thms ("pnat_mult_ac", [pnat_mult_assoc, pnat_mult_commute, pnat_mult_left_commute]);
   15.54  
   15.55  Goal "!!i j k::pnat. i<=j ==> i * k <= j * k";
   15.56  by (asm_full_simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
    16.1 --- a/src/HOL/Real/PRat.ML	Thu Jun 22 11:37:13 2000 +0200
    16.2 +++ b/src/HOL/Real/PRat.ML	Thu Jun 22 23:04:34 2000 +0200
    16.3 @@ -59,7 +59,7 @@
    16.4                         addSEs [sym, prat_trans_lemma]) 1);
    16.5  qed "equiv_ratrel";
    16.6  
    16.7 -val equiv_ratrel_iff = [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff;
    16.8 +bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
    16.9  
   16.10  Goalw  [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat";
   16.11  by (Blast_tac 1);
   16.12 @@ -74,7 +74,7 @@
   16.13            ratrel_iff, ratrel_in_prat, Abs_prat_inverse];
   16.14  
   16.15  Addsimps [equiv_ratrel RS eq_equiv_class_iff];
   16.16 -val eq_ratrelD = equiv_ratrel RSN (2,eq_equiv_class);
   16.17 +bind_thm ("eq_ratrelD", equiv_ratrel RSN (2,eq_equiv_class));
   16.18  
   16.19  Goal "inj(Rep_prat)";
   16.20  by (rtac inj_inverseI 1);
   16.21 @@ -182,7 +182,7 @@
   16.22  qed "prat_add_left_commute";
   16.23  
   16.24  (* Positive Rational addition is an AC operator *)
   16.25 -val prat_add_ac = [prat_add_assoc, prat_add_commute, prat_add_left_commute];
   16.26 +bind_thms ("prat_add_ac", [prat_add_assoc, prat_add_commute, prat_add_left_commute]);
   16.27  
   16.28  
   16.29  (*** Congruence property for multiplication ***)
   16.30 @@ -228,8 +228,8 @@
   16.31  qed "prat_mult_left_commute";
   16.32  
   16.33  (*Positive Rational multiplication is an AC operator*)
   16.34 -val prat_mult_ac = [prat_mult_assoc,
   16.35 -                    prat_mult_commute,prat_mult_left_commute];
   16.36 +bind_thms ("prat_mult_ac", [prat_mult_assoc,
   16.37 +                    prat_mult_commute,prat_mult_left_commute]);
   16.38  
   16.39  Goalw [prat_of_pnat_def] 
   16.40        "(prat_of_pnat (Abs_pnat 1)) * z = z";
   16.41 @@ -572,7 +572,7 @@
   16.42  by (assume_tac 1);
   16.43  qed "prat_leD";
   16.44  
   16.45 -val prat_leE = make_elim prat_leD;
   16.46 +bind_thm ("prat_leE", make_elim prat_leD);
   16.47  
   16.48  Goal "(~(w < z)) = (z <= (w::prat))";
   16.49  by (fast_tac (claset() addSIs [prat_leI,prat_leD]) 1);
    17.1 --- a/src/HOL/Real/PReal.ML	Thu Jun 22 11:37:13 2000 +0200
    17.2 +++ b/src/HOL/Real/PReal.ML	Thu Jun 22 23:04:34 2000 +0200
    17.3 @@ -281,7 +281,7 @@
    17.4             rtac (preal_add_commute RS arg_cong) 1]);
    17.5  
    17.6  (* Positive Reals addition is an AC operator *)
    17.7 -val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
    17.8 +bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
    17.9  
   17.10    (*** Properties of multiplication ***)
   17.11  
   17.12 @@ -367,9 +367,9 @@
   17.13             rtac (preal_mult_commute RS arg_cong) 1]);
   17.14  
   17.15  (* Positive Reals multiplication is an AC operator *)
   17.16 -val preal_mult_ac = [preal_mult_assoc, 
   17.17 +bind_thms ("preal_mult_ac", [preal_mult_assoc, 
   17.18                       preal_mult_commute, 
   17.19 -                     preal_mult_left_commute];
   17.20 +                     preal_mult_left_commute]);
   17.21  
   17.22  (* Positive Real 1 is the multiplicative identity element *) 
   17.23  (* long *)
   17.24 @@ -746,7 +746,7 @@
   17.25  by (auto_tac  (claset() addDs [equalityI],simpset()));
   17.26  qed "preal_leD";
   17.27  
   17.28 -val preal_leE = make_elim preal_leD;
   17.29 +bind_thm ("preal_leE", make_elim preal_leD);
   17.30  
   17.31  Goalw [preal_le_def,psubset_def,preal_less_def]
   17.32                     "~ z <= w ==> w<(z::preal)";
    18.1 --- a/src/HOL/Real/ROOT.ML	Thu Jun 22 11:37:13 2000 +0200
    18.2 +++ b/src/HOL/Real/ROOT.ML	Thu Jun 22 23:04:34 2000 +0200
    18.3 @@ -1,4 +1,4 @@
    18.4 -(*  Title:      HOL/Real/ROOT
    18.5 +(*  Title:      HOL/Real/ROOT.ML
    18.6      ID:         $Id$
    18.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    18.8      Copyright   1998  University of Cambridge
    18.9 @@ -8,5 +8,4 @@
   18.10  Linear real arithmetic is installed in RealBin.ML.
   18.11  *)
   18.12  
   18.13 -time_use_thy "Real";
   18.14 -time_use_thy "Hyperreal/HyperDef";
   18.15 +with_path "Hyperreal" use_thy "HyperDef";
    19.1 --- a/src/HOL/Real/RealBin.ML	Thu Jun 22 11:37:13 2000 +0200
    19.2 +++ b/src/HOL/Real/RealBin.ML	Thu Jun 22 23:04:34 2000 +0200
    19.3 @@ -349,7 +349,7 @@
    19.4  		   real_mult_minus_1, real_mult_minus_1_right];
    19.5  
    19.6  (*To perform binary arithmetic*)
    19.7 -val bin_simps = 
    19.8 +val bin_simps =
    19.9      [add_real_number_of, real_add_number_of_left, minus_real_number_of, 
   19.10       diff_real_number_of] @ 
   19.11      bin_arith_simps @ bin_rel_simps;
    20.1 --- a/src/HOL/Real/RealDef.ML	Thu Jun 22 11:37:13 2000 +0200
    20.2 +++ b/src/HOL/Real/RealDef.ML	Thu Jun 22 23:04:34 2000 +0200
    20.3 @@ -56,10 +56,10 @@
    20.4                        addSEs [sym,preal_trans_lemma]) 1);
    20.5  qed "equiv_realrel";
    20.6  
    20.7 -val equiv_realrel_iff =
    20.8 +bind_thm ("equiv_realrel_iff",
    20.9      [TrueI, TrueI] MRS 
   20.10      ([CollectI, CollectI] MRS 
   20.11 -    (equiv_realrel RS eq_equiv_class_iff));
   20.12 +    (equiv_realrel RS eq_equiv_class_iff)));
   20.13  
   20.14  Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
   20.15  by (Blast_tac 1);
   20.16 @@ -74,7 +74,7 @@
   20.17            realrel_iff, realrel_in_real, Abs_real_inverse];
   20.18  
   20.19  Addsimps [equiv_realrel RS eq_equiv_class_iff];
   20.20 -val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
   20.21 +bind_thm ("eq_realrelD", equiv_realrel RSN (2,eq_equiv_class));
   20.22  
   20.23  Goal "inj(Rep_real)";
   20.24  by (rtac inj_inverseI 1);
   20.25 @@ -1081,11 +1081,11 @@
   20.26  (*This list of rewrites simplifies (in)equalities by bringing subtractions
   20.27    to the top and then moving negative terms to the other side.  
   20.28    Use with real_add_ac*)
   20.29 -val real_compare_rls = 
   20.30 +bind_thms ("real_compare_rls",
   20.31    [symmetric real_diff_def,
   20.32     real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2, 
   20.33     real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq, 
   20.34 -   real_diff_eq_eq, real_eq_diff_eq];
   20.35 +   real_diff_eq_eq, real_eq_diff_eq]);
   20.36  
   20.37  
   20.38  (** For the cancellation simproc.
    21.1 --- a/src/HOL/Relation.ML	Thu Jun 22 11:37:13 2000 +0200
    21.2 +++ b/src/HOL/Relation.ML	Thu Jun 22 23:04:34 2000 +0200
    21.3 @@ -45,7 +45,7 @@
    21.4  by (Blast_tac 1);
    21.5  qed "diag_eqI";
    21.6  
    21.7 -val diagI = refl RS diag_eqI |> standard;
    21.8 +bind_thm ("diagI", refl RS diag_eqI |> standard);
    21.9  
   21.10  (*The general elimination rule*)
   21.11  val major::prems = Goalw [diag_def]
    22.1 --- a/src/HOL/Set.ML	Thu Jun 22 11:37:13 2000 +0200
    22.2 +++ b/src/HOL/Set.ML	Thu Jun 22 23:04:34 2000 +0200
    22.3 @@ -31,7 +31,7 @@
    22.4  by (rtac (prem RS ext RS arg_cong) 1);
    22.5  qed "Collect_cong";
    22.6  
    22.7 -val CollectE = make_elim CollectD;
    22.8 +bind_thm ("CollectE", make_elim CollectD);
    22.9  
   22.10  AddSIs [CollectI];
   22.11  AddSEs [CollectE];
   22.12 @@ -191,7 +191,7 @@
   22.13  by (rtac set_ext 1);
   22.14  by (blast_tac (claset() addIs [subsetD]) 1);
   22.15  qed "subset_antisym";
   22.16 -val equalityI = subset_antisym;
   22.17 +bind_thm ("equalityI", subset_antisym);
   22.18  
   22.19  AddSIs [equalityI];
   22.20  
   22.21 @@ -325,8 +325,8 @@
   22.22  qed "PowD";
   22.23  
   22.24  
   22.25 -val Pow_bottom = empty_subsetI RS PowI;        (* {}: Pow(B) *)
   22.26 -val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
   22.27 +bind_thm ("Pow_bottom", empty_subsetI RS PowI);        (* {}: Pow(B) *)
   22.28 +bind_thm ("Pow_top", subset_refl RS PowI);             (* A : Pow(A) *)
   22.29  
   22.30  
   22.31  section "Set complement";
   22.32 @@ -348,7 +348,7 @@
   22.33  by (etac CollectD 1);
   22.34  qed "ComplD";
   22.35  
   22.36 -val ComplE = make_elim ComplD;
   22.37 +bind_thm ("ComplE", make_elim ComplD);
   22.38  
   22.39  AddSIs [ComplI];
   22.40  AddSEs [ComplE];
   22.41 @@ -720,13 +720,13 @@
   22.42  bind_thm ("split_if_mem2", 
   22.43      read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
   22.44  
   22.45 -val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
   22.46 -		  split_if_mem1, split_if_mem2];
   22.47 +bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
   22.48 +		  split_if_mem1, split_if_mem2]);
   22.49  
   22.50  
   22.51  (*Each of these has ALREADY been added to simpset() above.*)
   22.52 -val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
   22.53 -                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
   22.54 +bind_thms ("mem_simps", [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
   22.55 +                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]);
   22.56  
   22.57  (*Would like to add these, but the existing code only searches for the 
   22.58    outer-level constant, which in this case is just "op :"; we instead need
    23.1 --- a/src/HOL/Sum.ML	Thu Jun 22 11:37:13 2000 +0200
    23.2 +++ b/src/HOL/Sum.ML	Thu Jun 22 23:04:34 2000 +0200
    23.3 @@ -43,8 +43,7 @@
    23.4  AddIffs [Inl_not_Inr, Inr_not_Inl];
    23.5  
    23.6  bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
    23.7 -
    23.8 -val Inr_neq_Inl = sym RS Inl_neq_Inr;
    23.9 +bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr);
   23.10  
   23.11  
   23.12  (** Injectiveness of Inl and Inr **)
   23.13 @@ -65,7 +64,7 @@
   23.14  by (rtac Inl_RepI 1);
   23.15  by (rtac Inl_RepI 1);
   23.16  qed "inj_Inl";
   23.17 -val Inl_inject = inj_Inl RS injD;
   23.18 +bind_thm ("Inl_inject", inj_Inl RS injD);
   23.19  
   23.20  Goalw [Inr_def] "inj(Inr)";
   23.21  by (rtac injI 1);
   23.22 @@ -73,7 +72,7 @@
   23.23  by (rtac Inr_RepI 1);
   23.24  by (rtac Inr_RepI 1);
   23.25  qed "inj_Inr";
   23.26 -val Inr_inject = inj_Inr RS injD;
   23.27 +bind_thm ("Inr_inject", inj_Inr RS injD);
   23.28  
   23.29  Goal "(Inl(x)=Inl(y)) = (x=y)";
   23.30  by (blast_tac (claset() addSDs [Inl_inject]) 1);
   23.31 @@ -138,7 +137,7 @@
   23.32  by (Blast_tac 1);
   23.33  qed "Part_eqI";
   23.34  
   23.35 -val PartI = refl RSN (2,Part_eqI);
   23.36 +bind_thm ("PartI", refl RSN (2,Part_eqI));
   23.37  
   23.38  val major::prems = Goalw [Part_def]
   23.39      "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
    24.1 --- a/src/HOL/Trancl.ML	Thu Jun 22 11:37:13 2000 +0200
    24.2 +++ b/src/HOL/Trancl.ML	Thu Jun 22 23:04:34 2000 +0200
    24.3 @@ -15,7 +15,7 @@
    24.4  by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    24.5  qed "rtrancl_fun_mono";
    24.6  
    24.7 -val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
    24.8 +bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski));
    24.9  
   24.10  (*Reflexivity of rtrancl*)
   24.11  Goal "(a,a) : r^*";
    25.1 --- a/src/HOL/Univ.ML	Thu Jun 22 11:37:13 2000 +0200
    25.2 +++ b/src/HOL/Univ.ML	Thu Jun 22 23:04:34 2000 +0200
    25.3 @@ -61,7 +61,7 @@
    25.4  by (etac Abs_Node_inverse 1);
    25.5  qed "inj_on_Abs_Node";
    25.6  
    25.7 -val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
    25.8 +bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
    25.9  
   25.10  
   25.11  (*** Introduction rules for Node ***)
   25.12 @@ -98,7 +98,7 @@
   25.13  Goalw [Atom_def] "inj(Atom)";
   25.14  by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
   25.15  qed "inj_Atom";
   25.16 -val Atom_inject = inj_Atom RS injD;
   25.17 +bind_thm ("Atom_inject", inj_Atom RS injD);
   25.18  
   25.19  Goal "(Atom(a)=Atom(b)) = (a=b)";
   25.20  by (blast_tac (claset() addSDs [Atom_inject]) 1);
   25.21 @@ -118,7 +118,7 @@
   25.22  by (etac (Atom_inject RS Inr_inject) 1);
   25.23  qed "inj_Numb";
   25.24  
   25.25 -val Numb_inject = inj_Numb RS injD;
   25.26 +bind_thm ("Numb_inject", inj_Numb RS injD);
   25.27  AddSDs [Numb_inject];
   25.28  
   25.29  (** Injectiveness of Push_Node **)
   25.30 @@ -586,7 +586,7 @@
   25.31  by (Blast_tac 1);
   25.32  qed "dprod_Sigma";
   25.33  
   25.34 -val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
   25.35 +bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
   25.36  
   25.37  (*Dependent version*)
   25.38  Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
   25.39 @@ -599,7 +599,7 @@
   25.40  by (Blast_tac 1);
   25.41  qed "dsum_Sigma";
   25.42  
   25.43 -val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
   25.44 +bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
   25.45  
   25.46  
   25.47  (*** Domain ***)
    26.1 --- a/src/HOL/WF.ML	Thu Jun 22 11:37:13 2000 +0200
    26.2 +++ b/src/HOL/WF.ML	Thu Jun 22 23:04:34 2000 +0200
    26.3 @@ -68,6 +68,8 @@
    26.4  "!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [
    26.5  	stac (trancl_converse RS sym) 1,
    26.6  	etac wf_trancl 1]);
    26.7 +bind_thm ("wf_converse_trancl", wf_converse_trancl);
    26.8 +
    26.9  
   26.10  (*----------------------------------------------------------------------------
   26.11   * Minimal-element characterization of well-foundedness
    27.1 --- a/src/HOL/WF_Rel.ML	Thu Jun 22 11:37:13 2000 +0200
    27.2 +++ b/src/HOL/WF_Rel.ML	Thu Jun 22 23:04:34 2000 +0200
    27.3 @@ -66,7 +66,7 @@
    27.4  val measure_induct = standard
    27.5      (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
    27.6        (wf_measure RS wf_induct));
    27.7 -store_thm("measure_induct",measure_induct);
    27.8 +bind_thm ("measure_induct", measure_induct);
    27.9  
   27.10  (*----------------------------------------------------------------------------
   27.11   * Wellfoundedness of lexicographic combinations