Finite.ML

--- a/Finite.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Finite.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -11,11 +11,11 @@
 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
 br lfp_mono 1;
 by (REPEAT (ares_tac basic_monos 1));
-val Fin_mono = result();
+qed "Fin_mono";
 
 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
 by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
-val Fin_subset_Pow = result();
+qed "Fin_subset_Pow";
 
 (* A : Fin(B) ==> A <= B *)
 val FinD = Fin_subset_Pow RS subsetD RS PowD;
@@ -29,7 +29,7 @@
 by (excluded_middle_tac "a:b" 2);
 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
 by (REPEAT (ares_tac prems 1));
-val Fin_induct = result();
+qed "Fin_induct";
 
 (** Simplification for Fin **)
 
@@ -40,7 +40,7 @@
     "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
 by (rtac (major RS Fin_induct) 1);
 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
-val Fin_UnI = result();
+qed "Fin_UnI";
 
 (*Every subset of a finite set is finite*)
 val [subs,fin] = goal Finite.thy "[| A<=B;  B: Fin(M) |] ==> A: Fin(M)";
@@ -52,7 +52,7 @@
 by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
 by (ALLGOALS (asm_simp_tac Fin_ss));
-val Fin_subset = result();
+qed "Fin_subset";
 
 (*The image of a finite set is finite*)
 val major::_ = goal Finite.thy
@@ -60,7 +60,7 @@
 by (rtac (major RS Fin_induct) 1);
 by (simp_tac Fin_ss 1);
 by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
-val Fin_imageI = result();
+qed "Fin_imageI";
 
 val major::prems = goal Finite.thy 
     "[| c: Fin(A);  b: Fin(A);  				\
@@ -71,7 +71,7 @@
 by (rtac (Diff_insert RS ssubst) 2);
 by (ALLGOALS (asm_simp_tac
                 (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
-val Fin_empty_induct_lemma = result();
+qed "Fin_empty_induct_lemma";
 
 val prems = goal Finite.thy 
     "[| b: Fin(A);  						\
@@ -81,4 +81,4 @@
 by (rtac (Diff_cancel RS subst) 1);
 by (rtac (Fin_empty_induct_lemma RS mp) 1);
 by (REPEAT (ares_tac (subset_refl::prems) 1));
-val Fin_empty_induct = result();
+qed "Fin_empty_induct";