ex/Simult.ML

--- a/ex/Simult.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/ex/Simult.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -155,37 +155,37 @@
 goalw Simult.thy TF_Rep_defs "(TCONS(K,M)=TCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_TCONS_eq";
-val TCONS_inject = standard (TCONS_TCONS_eq RS iffD1 RS conjE);
+bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
 
 goalw Simult.thy TF_Rep_defs "(FCONS(K,M)=FCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
 qed "FCONS_FCONS_eq";
-val FCONS_inject = standard (FCONS_FCONS_eq RS iffD1 RS conjE);
+bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_not_FNIL";
-val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
+bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
 
-val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
+bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
 val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "FCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 qed "FCONS_not_FNIL";
-val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
+bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
 
-val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
+bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
 val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FCONS(K,L)";
 by (fast_tac TF_Rep_cs 1);
 qed "TCONS_not_FCONS";
-val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
+bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
 
-val TCONS_neq_FCONS = standard (TCONS_not_FCONS RS notE);
+bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
 val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
 
 (*???? Too many derived rules ????
@@ -207,13 +207,13 @@
 goalw Simult.thy [Tcons_def] "(Tcons(x,xs)=Tcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
 qed "Tcons_Tcons_eq";
-val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
+bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
 
 goalw Simult.thy [Fcons_def,Fnil_def] "Fcons(x,xs) ~= Fnil";
 by (fast_tac TF_cs 1);
 qed "Fcons_not_Fnil";
 
-val Fcons_neq_Fnil = standard (Fcons_not_Fnil RS notE);;
+bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
 val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
 
 
@@ -222,7 +222,7 @@
 goalw Simult.thy [Fcons_def] "(Fcons(x,xs)=Fcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
 qed "Fcons_Fcons_eq";
-val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
+bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
 
 
 (*** TF_rec -- by wf recursion on pred_sexp ***)