diff -r 3a8d722fd3ff -r 16c4ea954511 Subst/UTerm.ML
--- a/Subst/UTerm.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Subst/UTerm.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -15,21 +15,21 @@
 by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs)
                       addEs [rew uterm.elim]) 1)
 end;
-val uterm_unfold = result();
+qed "uterm_unfold";
 
 (** the uterm functional **)
 
 (*This justifies using uterm in other recursive type definitions*)
 goalw UTerm.thy uterm.defs "!!A B. A<=B ==> uterm(A) <= uterm(B)";
 by (REPEAT (ares_tac (lfp_mono::basic_monos) 1));
-val uterm_mono = result();
+qed "uterm_mono";
 
 (** Type checking rules -- uterm creates well-founded sets **)
 
 goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
 by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
-val uterm_sexp = result();
+qed "uterm_sexp";
 
 (* A <= sexp ==> uterm(A) <= sexp *)
 val uterm_subset_sexp = standard ([uterm_mono, uterm_sexp] MRS subset_trans);
@@ -44,7 +44,7 @@
 by (rtac (Rep_uterm RS uterm.induct) 1);
 by (REPEAT (ares_tac prems 1
      ORELSE eresolve_tac [rangeE, ssubst, Abs_uterm_inverse RS subst] 1));
-val uterm_induct = result();
+qed "uterm_induct";
 
 (*Perform induction on xs. *)
 fun uterm_ind_tac a M = 
@@ -57,33 +57,33 @@
 goal UTerm.thy "inj(Rep_uterm)";
 by (rtac inj_inverseI 1);
 by (rtac Rep_uterm_inverse 1);
-val inj_Rep_uterm = result();
+qed "inj_Rep_uterm";
 
 goal UTerm.thy "inj_onto(Abs_uterm,uterm(range(Leaf)))";
 by (rtac inj_onto_inverseI 1);
 by (etac Abs_uterm_inverse 1);
-val inj_onto_Abs_uterm = result();
+qed "inj_onto_Abs_uterm";
 
 (** Distinctness of constructors **)
 
 goalw UTerm.thy uterm_con_defs "~ CONST(c) = COMB(u,v)";
 by (rtac notI 1);
 by (etac (In1_inject RS (In0_not_In1 RS notE)) 1);
-val CONST_not_COMB = result();
+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);
 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);
-val COMB_not_VAR = result();
+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);
 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);
-val VAR_not_CONST = result();
+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);
 val CONST_neq_VAR = sym RS VAR_neq_CONST;
@@ -92,7 +92,7 @@
 goalw UTerm.thy [Const_def,Comb_def] "~ Const(c) = Comb(u,v)";
 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));
-val Const_not_Comb = result();
+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);
 val Comb_neq_Const = sym RS Const_neq_Comb;
@@ -100,7 +100,7 @@
 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));
-val Comb_not_Var = result();
+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);
 val Var_neq_Comb = sym RS Comb_neq_Var;
@@ -108,7 +108,7 @@
 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));
-val Var_not_Const = result();
+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);
 val Const_neq_Var = sym RS Var_neq_Const;
@@ -121,15 +121,15 @@
 
 goalw UTerm.thy [VAR_def] "(VAR(M)=VAR(N)) = (M=N)";
 by (fast_tac inject_cs 1);
-val VAR_VAR_eq = result();
+qed "VAR_VAR_eq";
 
 goalw UTerm.thy [CONST_def] "(CONST(M)=CONST(N)) = (M=N)";
 by (fast_tac inject_cs 1);
-val CONST_CONST_eq = result();
+qed "CONST_CONST_eq";
 
 goalw UTerm.thy [COMB_def] "(COMB(K,L)=COMB(M,N)) = (K=M & L=N)";
 by (fast_tac inject_cs 1);
-val COMB_COMB_eq = result();
+qed "COMB_COMB_eq";
 
 val VAR_inject = standard (VAR_VAR_eq RS iffD1);
 val CONST_inject = standard (CONST_CONST_eq RS iffD1);
@@ -147,37 +147,37 @@
 
 goalw UTerm.thy [Var_def] "(Var(x)=Var(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
-val Var_Var_eq = result();
+qed "Var_Var_eq";
 val Var_inject = standard (Var_Var_eq RS iffD1);
 
 goalw UTerm.thy [Const_def] "(Const(x)=Const(y)) = (x=y)";
 by (fast_tac uterm_cs 1);
-val Const_Const_eq = result();
+qed "Const_Const_eq";
 val Const_inject = standard (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);
-val Comb_Comb_eq = result();
+qed "Comb_Comb_eq";
 val Comb_inject = standard (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);
 by (etac uterm.induct 1);
 by (ALLGOALS (fast_tac uterm_cs));
-val VAR_D = result();
+qed "VAR_D";
 
 val [major] = goal UTerm.thy "CONST(M): uterm(A) ==> M : A";
 by (rtac (major RS setup_induction) 1);
 by (etac uterm.induct 1);
 by (ALLGOALS (fast_tac uterm_cs));
-val CONST_D = result();
+qed "CONST_D";
 
 val [major] = goal UTerm.thy
     "COMB(M,N): uterm(A) ==> M: uterm(A) & N: uterm(A)";
 by (rtac (major RS setup_induction) 1);
 by (etac uterm.induct 1);
 by (ALLGOALS (fast_tac uterm_cs));
-val COMB_D = result();
+qed "COMB_D";
 
 (*Basic ss with constructors and their freeness*)
 val uterm_free_simps = uterm.intrs @
@@ -194,14 +194,14 @@
 by (rtac (Var_not_Comb RS allI) 1);
 by (rtac (Const_not_Comb RS allI) 1);
 by (asm_simp_tac uterm_free_ss 1);
-val t_not_Comb_t = result();
+qed "t_not_Comb_t";
 
 goal UTerm.thy "!t. u~=Comb(t,u)";
 by (uterm_ind_tac "u" 1);
 by (rtac (Var_not_Comb RS allI) 1);
 by (rtac (Const_not_Comb RS allI) 1);
 by (asm_simp_tac uterm_free_ss 1);
-val u_not_Comb_u = result();
+qed "u_not_Comb_u";
 
 
 (*** UTerm_rec -- by wf recursion on pred_sexp ***)
@@ -214,12 +214,12 @@
 goalw UTerm.thy [VAR_def] "UTerm_rec(VAR(x),b,c,d) = b(x)";
 by (rtac (UTerm_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In0]) 1);
-val UTerm_rec_VAR = result();
+qed "UTerm_rec_VAR";
 
 goalw UTerm.thy [CONST_def] "UTerm_rec(CONST(x),b,c,d) = c(x)";
 by (rtac (UTerm_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1);
-val UTerm_rec_CONST = result();
+qed "UTerm_rec_CONST";
 
 goalw UTerm.thy [COMB_def]
     "!!M N. [| M: sexp;  N: sexp |] ==> 	\
@@ -228,7 +228,7 @@
 by (rtac (UTerm_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
 by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1);
-val UTerm_rec_COMB = result();
+qed "UTerm_rec_COMB";
 
 (*** uterm_rec -- by UTerm_rec ***)
 
@@ -244,16 +244,16 @@
 
 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec(Var(x),b,c,d) = b(x)";
 by (simp_tac uterm_rec_ss 1);
-val uterm_rec_Var = result();
+qed "uterm_rec_Var";
 
 goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec(Const(x),b,c,d) = c(x)";
 by (simp_tac uterm_rec_ss 1);
-val uterm_rec_Const = result();
+qed "uterm_rec_Const";
 
 goalw UTerm.thy [uterm_rec_def, Comb_def]
    "uterm_rec(Comb(u,v),b,c,d) = d(u,v,uterm_rec(u,b,c,d),uterm_rec(v,b,c,d))";
 by (simp_tac uterm_rec_ss 1);
-val uterm_rec_Comb = result();
+qed "uterm_rec_Comb";
 
 val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB,
 		 uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb];