diff -r 3a8d722fd3ff -r 16c4ea954511 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";