# HG changeset patch
# User clasohm
# Date 799496537 -7200
# Node ID c1ccf6679a96ca4e47ad4d8aa3ae19a26a6fb6b1
# Parent  46a7b619e62e2bcc7a90aa8003064e95bd348876
replaced store_thm by bind_thm

diff -r 46a7b619e62e -r c1ccf6679a96 src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Wed May 03 12:17:30 1995 +0200
+++ b/src/CCL/CCL.ML	Wed May 03 12:22:17 1995 +0200
@@ -26,7 +26,7 @@
 goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
 by (fast_tac (set_cs addIs [po_abstractn]) 1);
-val abstractn = store_thm("abstractn", standard (allI RS (result() RS mp)));
+bind_thm("abstractn", standard (allI RS (result() RS mp)));
 
 fun type_of_terms (Const("Trueprop",_) $ 
                    (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
@@ -143,7 +143,7 @@
 
 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
 by (fast_tac ccl_cs 1);
-val XHlemma2 = store_thm("XHlemma2", result() RS mp);
+bind_thm("XHlemma2", result() RS mp);
 
 (*** Pre-Order ***)
 
@@ -182,7 +182,7 @@
 by (dtac (poXH RS iffD1) 1);
 by (etac rev_mp 1);
 by (simp_tac ccl_ss 1);
-val bot_poleast = store_thm("bot_poleast", result() RS mp);
+bind_thm("bot_poleast", result() RS mp);
 
 goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
 by (rtac (poXH RS iff_trans) 1);
@@ -318,7 +318,7 @@
 goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
 by (safe_tac ccl_cs);
 by (simp_tac ccl_ss 1);
-val cond_eta = store_thm("cond_eta", result() RS mp);
+bind_thm("cond_eta", result() RS mp);
 
 goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
diff -r 46a7b619e62e -r c1ccf6679a96 src/CCL/Term.ML
--- a/src/CCL/Term.ML	Wed May 03 12:17:30 1995 +0200
+++ b/src/CCL/Term.ML	Wed May 03 12:22:17 1995 +0200
@@ -24,7 +24,7 @@
 goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
 by (res_inst_tac [("t","t")] term_case 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val letB = store_thm("letB", result() RS mp);
+bind_thm("letB", result() RS mp);
 
 goalw Term.thy [let_def] "let x be bot in f(x) = bot";
 by (rtac caseBbot 1);
diff -r 46a7b619e62e -r c1ccf6679a96 src/CCL/Type.ML
--- a/src/CCL/Type.ML	Wed May 03 12:17:30 1995 +0200
+++ b/src/CCL/Type.ML	Wed May 03 12:22:17 1995 +0200
@@ -159,18 +159,18 @@
 goal Type.thy "mono(%X.Unit+X)";
 by (REPEAT (ares_tac [PlusM,constM,idM] 1));
 qed "NatM";
-val def_NatB = store_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
+bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
 
 goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "ListM";
-val def_ListB = store_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
-val def_ListsB = store_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
+bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
+bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
 
 goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "IListsM";
-val def_IListsB = store_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
+bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
 
 val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];