ex/Term.ML

--- a/ex/Term.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/Term.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -14,19 +14,19 @@
 goal Term.thy "term(A) = A <*> list(term(A))";
 by (fast_tac (univ_cs addSIs (equalityI :: term.intrs)
                       addEs [term.elim]) 1);
-val term_unfold = result();
+qed "term_unfold";
 
 (*This justifies using term in other recursive type definitions*)
 goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
 by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
-val term_mono = result();
+qed "term_mono";
 
 (** Type checking -- term creates well-founded sets **)
 
 goalw Term.thy term.defs "term(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
 by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
-val term_sexp = result();
+qed "term_sexp";
 
 (* A <= sexp ==> term(A) <= sexp *)
 val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans);
@@ -56,7 +56,7 @@
 by (rtac (major RS term_induct) 1);
 by (etac list.induct 1);
 by (REPEAT (ares_tac prems 1));
-val term_induct2 = result();
+qed "term_induct2";
 
 (*** Structural Induction on the abstract type 'a term ***)
 
@@ -90,7 +90,7 @@
 by (rtac list_subset_sexp 2);
 by (fast_tac set_cs 2);
 by (ALLGOALS (asm_simp_tac list_all_ss));
-val term_induct = result();
+qed "term_induct";
 
 (*Induction for the abstract type 'a term*)
 val prems = goal Term.thy 
@@ -101,7 +101,7 @@
 by (etac rev_mp 1);
 by (rtac list_induct 1);  (*types force good instantiation*)
 by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems)));
-val term_induct2 = result();
+qed "term_induct2";
 
 (*Perform induction on xs. *)
 fun term_ind2_tac a i = 
@@ -127,7 +127,7 @@
 by (strip_tac 1);
 by (etac (pred_sexp_CONS_D RS conjE) 1);
 by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1);
-val Abs_map_lemma = result();
+qed "Abs_map_lemma";
 
 val [prem1,prem2,A_subset_sexp] = goal Term.thy
     "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
@@ -138,7 +138,7 @@
        prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
        prem1, prem2 RS rev_subsetD, list_subset_sexp,
        term_subset_sexp, A_subset_sexp])1);
-val Term_rec = result();
+qed "Term_rec";
 
 (*** term_rec -- by Term_rec ***)