Subst/UTerm.ML

--- a/Subst/UTerm.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/Subst/UTerm.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -32,7 +32,7 @@
 qed "uterm_sexp";
 
 (* A <= sexp ==> uterm(A) <= sexp *)
-val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans);
+bind_thm ("uterm_subset_sexp", ([uterm_mono, uterm_sexp] MRS subset_trans));
 
 (** Induction **)
 
@@ -70,22 +70,22 @@
 by (rtac notI 1);
 by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
 qed "CONST_not_COMB";
-val COMB_not_CONST = standard (CONST_not_COMB RS not_sym);
-val CONST_neq_COMB = standard (CONST_not_COMB RS notE);
+bind_thm ("COMB_not_CONST", (CONST_not_COMB RS not_sym));
+bind_thm ("CONST_neq_COMB", (CONST_not_COMB RS notE));
 val COMB_neq_CONST = sym RS CONST_neq_COMB;
 
 goalw UTerm.thy uterm_con_defs "~ COMB(u,v) = VAR(x)";
 by (rtac In1_not_In0 1);
 qed "COMB_not_VAR";
-val VAR_not_COMB = standard (COMB_not_VAR RS not_sym);
-val COMB_neq_VAR = standard (COMB_not_VAR RS notE);
+bind_thm ("VAR_not_COMB", (COMB_not_VAR RS not_sym));
+bind_thm ("COMB_neq_VAR", (COMB_not_VAR RS notE));
 val VAR_neq_COMB = sym RS COMB_neq_VAR;
 
 goalw UTerm.thy uterm_con_defs "~ VAR(x) = CONST(c)";
 by (rtac In0_not_In1 1);
 qed "VAR_not_CONST";
-val CONST_not_VAR = standard (VAR_not_CONST RS not_sym);
-val VAR_neq_CONST = standard (VAR_not_CONST RS notE);
+bind_thm ("CONST_not_VAR", (VAR_not_CONST RS not_sym));
+bind_thm ("VAR_neq_CONST", (VAR_not_CONST RS notE));
 val CONST_neq_VAR = sym RS VAR_neq_CONST;
 
 
@@ -93,24 +93,24 @@
 by (rtac (CONST_not_COMB RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Const_not_Comb";
-val Comb_not_Const = standard (Const_not_Comb RS not_sym);
-val Const_neq_Comb = standard (Const_not_Comb RS notE);
+bind_thm ("Comb_not_Const", (Const_not_Comb RS not_sym));
+bind_thm ("Const_neq_Comb", (Const_not_Comb RS notE));
 val Comb_neq_Const = sym RS Const_neq_Comb;
 
 goalw UTerm.thy [Comb_def,Var_def] "~ Comb(u,v) = Var(x)";
 by (rtac (COMB_not_VAR RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Comb_not_Var";
-val Var_not_Comb = standard (Comb_not_Var RS not_sym);
-val Comb_neq_Var = standard (Comb_not_Var RS notE);
+bind_thm ("Var_not_Comb", (Comb_not_Var RS not_sym));
+bind_thm ("Comb_neq_Var", (Comb_not_Var RS notE));
 val Var_neq_Comb = sym RS Comb_neq_Var;
 
 goalw UTerm.thy [Var_def,Const_def] "~ Var(x) = Const(c)";
 by (rtac (VAR_not_CONST RS (inj_onto_Abs_uterm RS inj_onto_contraD)) 1);
 by (REPEAT (resolve_tac (uterm.intrs @ [rangeI, Rep_uterm]) 1));
 qed "Var_not_Const";
-val Const_not_Var = standard (Var_not_Const RS not_sym);
-val Var_neq_Const = standard (Var_not_Const RS notE);
+bind_thm ("Const_not_Var", (Var_not_Const RS not_sym));
+bind_thm ("Var_neq_Const", (Var_not_Const RS notE));
 val Const_neq_Var = sym RS Var_neq_Const;
 
 
@@ -131,9 +131,9 @@
 by (fast_tac inject_cs 1);
 qed "COMB_COMB_eq";
 
-val VAR_inject = standard (VAR_VAR_eq RS iffD1);
-val CONST_inject = standard (CONST_CONST_eq RS iffD1);
-val COMB_inject = standard (COMB_COMB_eq RS iffD1 RS conjE);
+bind_thm ("VAR_inject", (VAR_VAR_eq RS iffD1));
+bind_thm ("CONST_inject", (CONST_CONST_eq RS iffD1));
+bind_thm ("COMB_inject", (COMB_COMB_eq RS iffD1 RS conjE));
 
 
 (*For reasoning about abstract uterm constructors*)
@@ -148,17 +148,17 @@
 goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
 qed "Var_Var_eq";
-val Var_inject = standard (Var_Var_eq RS iffD1);
+bind_thm ("Var_inject", (Var_Var_eq RS iffD1));
 
 goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
 qed "Const_Const_eq";
-val Const_inject = standard (Const_Const_eq RS iffD1);
+bind_thm ("Const_inject", (Const_Const_eq RS iffD1));
 
 goalw UTerm.thy [Comb_def] "(Comb(u,v)=Comb(x,y)) = (u=x & v=y)";
 by (fast_tac uterm_cs 1);
 qed "Comb_Comb_eq";
-val Comb_inject = standard (Comb_Comb_eq RS iffD1 RS conjE);
+bind_thm ("Comb_inject", (Comb_Comb_eq RS iffD1 RS conjE));
 
 val [major] = goal UTerm.thy "VAR(M): uterm(A) ==> M : A";
 by (rtac (major RS setup_induction) 1);