# HG changeset patch
# User clasohm
# Date 786887438 -3600
# Node ID ad45e477926cb3e4ce46b1edd653e4342bbb609e
# Parent  663cead79989dbca770304f661db30f8041ef628
replaced store_thm by bind_thm

diff -r 663cead79989 -r ad45e477926c IMP/Equiv.ML
--- a/IMP/Equiv.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/IMP/Equiv.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -9,13 +9,13 @@
 by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps)));	  (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
-val aexp_iff = store_thm("aexp_iff", result() RS spec);
+bind_thm("aexp_iff", result() RS spec);
 
 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))";
 by (bexp.induct_tac "b" 1);
 by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
               addsimps (aexp_iff::B_simps@evalb_simps))));
-val bexp_iff = store_thm("bexp_iff", result() RS spec);
+bind_thm("bexp_iff", result() RS spec);
 
 val bexp1 = bexp_iff RS iffD1;
 val bexp2 = bexp_iff RS iffD2;
diff -r 663cead79989 -r ad45e477926c IMP/Properties.ML
--- a/IMP/Properties.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/IMP/Properties.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -10,16 +10,14 @@
 goal Com.thy "!m n. <a,s> -a-> m & <a,s> -a-> n --> m=n";
 by(res_inst_tac[("aexp","a")]Com.aexp.induct 1);
 by(REPEAT(fast_tac (HOL_cs addSIs evala.intrs addSEs evala_elim_cases) 1));
-val aexp_detD =
-  store_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
+bind_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
 
 (* evaluation of bexp is deterministic *)
 goal Com.thy "!v w. <b,s> -b-> v & <b,s> -b-> w --> v=w";
 by(res_inst_tac[("bexp","b")]Com.bexp.induct 1);
 by(REPEAT(fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases
                            addDs [aexp_detD]) 1));
-val bexp_detD =
-  store_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
+bind_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
 
 
 val evalc_elim_cases = map (evalc.mk_cases com.simps)
diff -r 663cead79989 -r ad45e477926c List.ML
--- a/List.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/List.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -10,11 +10,10 @@
 
 val [Nil_not_Cons,Cons_not_Nil] = list.distinct;
 
-val Cons_neq_Nil = store_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
-val Nil_neq_Cons = store_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
+bind_thm("Cons_neq_Nil", standard (Cons_not_Nil RS notE));
+bind_thm("Nil_neq_Cons", sym RS Cons_neq_Nil);
 
-val Cons_inject =
-  store_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
+bind_thm("Cons_inject", standard ((hd list.inject) RS iffD1 RS conjE));
 
 val list_ss = HOL_ss addsimps list.simps;
 
diff -r 663cead79989 -r ad45e477926c ex/MT.ML
--- a/ex/MT.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/ex/MT.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -536,7 +536,7 @@
 
 goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
 by infsys_mono_tac;
-val mono_hasty_fun = store_thm("mono_hasty_fun",  result());
+bind_thm("mono_hasty_fun",  result());
 
 (* 
   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
diff -r 663cead79989 -r ad45e477926c ex/Puzzle.ML
--- a/ex/Puzzle.ML	Wed Dec 07 14:12:27 1994 +0100
+++ b/ex/Puzzle.ML	Thu Dec 08 12:50:38 1994 +0100
@@ -23,7 +23,7 @@
 by (subgoal_tac "f(na) <= f(f(na))" 1);
 by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
 by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
-val lemma = store_thm("lemma", result() RS spec RS mp);
+bind_thm("lemma", result() RS spec RS mp);
 
 goal Puzzle.thy "n <= f(n)";
 by (fast_tac (HOL_cs addIs [lemma]) 1);
@@ -38,7 +38,7 @@
 by (simp_tac nat_ss 1);
 by (simp_tac nat_ss 1);
 by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
-val mono_lemma1 = store_thm("mono_lemma1", result() RS mp);
+bind_thm("mono_lemma1", result() RS mp);
 
 val [p1,p2] = goal Puzzle.thy
     "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";