# HG changeset patch # User paulson # Date 1022850366 -7200 # Node ID 812b00ed1c03f780a4fcded0ea81b73893d7dadb # Parent d5234c261813b29a6884ac06b2adda126e4da9ab conversion of Finite to Isar format diff -r d5234c261813 -r 812b00ed1c03 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/CardinalArith.ML Fri May 31 15:06:06 2002 +0200 @@ -707,7 +707,7 @@ Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1); +by (simp_tac (simpset() addsimps [eqpoll_0_iff]) 1); by (Clarify_tac 1); by (subgoal_tac "EX u. u:A" 1); by (etac exE 1); @@ -716,7 +716,7 @@ by (assume_tac 1); by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); by (assume_tac 1); -by (resolve_tac [Fin.consI] 1); +by (resolve_tac [thm "Fin.consI"] 1); by (Blast_tac 1); by (blast_tac (claset() addIs [subset_consI RS Fin_mono RS subsetD]) 1); (*Now for the lemma assumed above*) @@ -729,7 +729,7 @@ qed "Finite_into_Fin"; Goal "A : Fin(U) ==> Finite(A)"; -by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1); +by (fast_tac (claset() addSIs [Finite_0, Finite_cons] addEs [Fin_induct]) 1); qed "Fin_into_Finite"; Goal "Finite(A) <-> A : Fin(A)"; @@ -746,9 +746,9 @@ Goal "[| ALL y:X. Finite(y); Finite(X) |] ==> Finite(Union(X))"; by (asm_full_simp_tac (simpset() addsimps [Finite_Fin_iff]) 1); by (rtac Fin_UnionI 1); -by (etac Fin.induct 1); +by (etac Fin_induct 1); by (Simp_tac 1); -by (blast_tac (claset() addIs [Fin.consI, impOfSubs Fin_mono]) 1); +by (blast_tac (claset() addIs [thm "Fin.consI", impOfSubs Fin_mono]) 1); qed "Finite_Union"; (* Induction principle for Finite(A), by Sidi Ehmety *) diff -r d5234c261813 -r 812b00ed1c03 src/ZF/Finite.ML --- a/src/ZF/Finite.ML Fri May 31 12:27:24 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,192 +0,0 @@ -(* Title: ZF/Finite.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Finite powerset operator; finite function space - -prove X:Fin(A) ==> |X| < nat - -prove: b: Fin(A) ==> inj(b,b)<=surj(b,b) -*) - -(*** Finite powerset operator ***) - -Goalw Fin.defs "A<=B ==> Fin(A) <= Fin(B)"; -by (rtac lfp_mono 1); -by (REPEAT (rtac Fin.bnd_mono 1)); -by (REPEAT (ares_tac (Pow_mono::basic_monos) 1)); -qed "Fin_mono"; - -(* A : Fin(B) ==> A <= B *) -bind_thm ("FinD", Fin.dom_subset RS subsetD RS PowD); - -(** Induction on finite sets **) - -(*Discharging x~:y entails extra work*) -val major::prems = Goal - "[| b: Fin(A); \ -\ P(0); \ -\ !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) \ -\ |] ==> P(b)"; -by (rtac (major RS Fin.induct) 1); -by (excluded_middle_tac "a:b" 2); -by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) -by (REPEAT (ares_tac prems 1)); -qed "Fin_induct"; - -(** Simplification for Fin **) -Addsimps Fin.intrs; - -(*The union of two finite sets is finite.*) -Goal "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; -by (etac Fin_induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons]))); -qed "Fin_UnI"; - -Addsimps [Fin_UnI]; - - -(*The union of a set of finite sets is finite.*) -Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; -by (etac Fin_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "Fin_UnionI"; - -(*Every subset of a finite set is finite.*) -Goal "b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)"; -by (etac Fin_induct 1); -by (simp_tac (simpset() addsimps [subset_empty_iff]) 1); -by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); -by Safe_tac; -by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); -by (Asm_simp_tac 1); -qed "Fin_subset_lemma"; - -Goal "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"; -by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1)); -qed "Fin_subset"; - -Goal "b: Fin(A) ==> b Int c : Fin(A)"; -by (blast_tac (claset() addIs [Fin_subset]) 1); -qed "Fin_IntI1"; - -Goal "c: Fin(A) ==> b Int c : Fin(A)"; -by (blast_tac (claset() addIs [Fin_subset]) 1); -qed "Fin_IntI2"; - -Addsimps[Fin_IntI1, Fin_IntI2]; -AddIs[Fin_IntI1, Fin_IntI2]; - - -val major::prems = Goal - "[| c: Fin(A); b: Fin(A); \ -\ P(b); \ -\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ -\ |] ==> c<=b --> P(b-c)"; -by (rtac (major RS Fin_induct) 1); -by (stac Diff_cons 2); -by (ALLGOALS (asm_simp_tac (simpset() addsimps (prems@[cons_subset_iff, - Diff_subset RS Fin_subset])))); -qed "Fin_0_induct_lemma"; - -val prems = Goal - "[| b: Fin(A); \ -\ P(b); \ -\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ -\ |] ==> P(0)"; -by (rtac (Diff_cancel RS subst) 1); -by (rtac (Fin_0_induct_lemma RS mp) 1); -by (REPEAT (ares_tac (subset_refl::prems) 1)); -qed "Fin_0_induct"; - -(*Functions from a finite ordinal*) -Goal "n: nat ==> n->A <= Fin(nat*A)"; -by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps [subset_iff]) 1); -by (asm_simp_tac - (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); -by (fast_tac (claset() addSIs [Fin.consI]) 1); -qed "nat_fun_subset_Fin"; - - -(*** Finite function space ***) - -Goalw FiniteFun.defs - "[| A<=C; B<=D |] ==> A -||> B <= C -||> D"; -by (rtac lfp_mono 1); -by (REPEAT (rtac FiniteFun.bnd_mono 1)); -by (REPEAT (ares_tac (Fin_mono::Sigma_mono::basic_monos) 1)); -qed "FiniteFun_mono"; - -Goal "A<=B ==> A -||> A <= B -||> B"; -by (REPEAT (ares_tac [FiniteFun_mono] 1)); -qed "FiniteFun_mono1"; - -Goal "h: A -||>B ==> h: domain(h) -> B"; -by (etac FiniteFun.induct 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1); -qed "FiniteFun_is_fun"; - -Goal "h: A -||>B ==> domain(h) : Fin(A)"; -by (etac FiniteFun.induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "FiniteFun_domain_Fin"; - -bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); - -(*Every subset of a finite function is a finite function.*) -Goal "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"; -by (etac FiniteFun.induct 1); -by (simp_tac (simpset() addsimps subset_empty_iff::FiniteFun.intrs) 1); -by (asm_simp_tac (simpset() addsimps subset_cons_iff::distrib_simps) 1); -by Safe_tac; -by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 1); -by (dtac (spec RS mp) 1 THEN assume_tac 1); -by (fast_tac (claset() addSIs FiniteFun.intrs) 1); -qed "FiniteFun_subset_lemma"; - -Goal "[| c<=b; b: A-||>B |] ==> c: A-||>B"; -by (REPEAT (ares_tac [FiniteFun_subset_lemma RS spec RS mp] 1)); -qed "FiniteFun_subset"; - -(** Some further results by Sidi O. Ehmety **) - -Goal "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"; -by (etac Fin.induct 1); -by (simp_tac (simpset() addsimps FiniteFun.intrs) 1); -by (Clarify_tac 1); -by (case_tac "a:b" 1); -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() addsimps [cons_absorb]) 1); -by (subgoal_tac "restrict(f,b) : b -||> B" 1); -by (blast_tac (claset() addIs [restrict_type2]) 2); -by (stac fun_cons_restrict_eq 1 THEN assume_tac 1); -by (full_simp_tac (simpset() addsimps [restrict_def, lam_def]) 1); -by (blast_tac (claset() addIs [apply_funtype, impOfSubs FiniteFun_mono] - @FiniteFun.intrs) 1); -qed_spec_mp "fun_FiniteFunI"; - -Goal "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}"; -by (blast_tac (claset() addIs [fun_FiniteFunI, lam_funtype]) 1); -qed "lam_FiniteFun"; - -Goal "f : FiniteFun(A, {y:B. P(y)}) \ -\ <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))"; -by Auto_tac; -by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1); -by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1); -by (res_inst_tac [("A1", "domain(f)")] - (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1); -by (fast_tac (claset() addDs - [FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1); -by (rtac fun_FiniteFunI 1); -by (etac FiniteFun_domain_Fin 1); -by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1); -by (ALLGOALS - (blast_tac (claset() addDs - [FiniteFun_is_fun, range_of_fun, range_type, - apply_equality]))); -qed "FiniteFun_Collect_iff"; diff -r d5234c261813 -r 812b00ed1c03 src/ZF/Finite.thy --- a/src/ZF/Finite.thy Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/Finite.thy Fri May 31 15:06:06 2002 +0200 @@ -3,36 +3,227 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Finite powerset operator +Finite powerset operator; finite function space + +prove X:Fin(A) ==> |X| < nat + +prove: b: Fin(A) ==> inj(b,b) <= surj(b,b) *) -Finite = Inductive + Epsilon + Nat + +theory Finite = Inductive + Epsilon + Nat: (*The natural numbers as a datatype*) -rep_datatype - elim natE - induct nat_induct - case_eqns nat_case_0, nat_case_succ - recursor_eqns recursor_0, recursor_succ +rep_datatype + elimination natE + induction nat_induct + case_eqns nat_case_0 nat_case_succ + recursor_eqns recursor_0 recursor_succ consts - Fin :: i=>i - FiniteFun :: [i,i]=>i ("(_ -||>/ _)" [61, 60] 60) + Fin :: "i=>i" + FiniteFun :: "[i,i]=>i" ("(_ -||>/ _)" [61, 60] 60) inductive domains "Fin(A)" <= "Pow(A)" - intrs - emptyI "0 : Fin(A)" - consI "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" - type_intrs empty_subsetI, cons_subsetI, PowI - type_elims "[make_elim PowD]" + intros + emptyI: "0 : Fin(A)" + consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)" + type_intros empty_subsetI cons_subsetI PowI + type_elims PowD [THEN revcut_rl] inductive domains "FiniteFun(A,B)" <= "Fin(A*B)" - intrs - emptyI "0 : A -||> B" - consI "[| a: A; b: B; h: A -||> B; a ~: domain(h) - |] ==> cons(,h) : A -||> B" - type_intrs "Fin.intrs" + intros + emptyI: "0 : A -||> B" + consI: "[| a: A; b: B; h: A -||> B; a ~: domain(h) |] + ==> cons(,h) : A -||> B" + type_intros Fin.intros + + +subsection {* Finite powerset operator *} + +lemma Fin_mono: "A<=B ==> Fin(A) <= Fin(B)" +apply (unfold Fin.defs) +apply (rule lfp_mono) +apply (rule Fin.bnd_mono)+ +apply blast +done + +(* A : Fin(B) ==> A <= B *) +lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard] + +(** Induction on finite sets **) + +(*Discharging x~:y entails extra work*) +lemma Fin_induct: + "[| b: Fin(A); + P(0); + !!x y. [| x: A; y: Fin(A); x~:y; P(y) |] ==> P(cons(x,y)) + |] ==> P(b)" +apply (erule Fin.induct, simp) +apply (case_tac "a:b") + apply (erule cons_absorb [THEN ssubst], assumption) (*backtracking!*) +apply simp +done + +(** Simplification for Fin **) +declare Fin.intros [simp] + +(*The union of two finite sets is finite.*) +lemma Fin_UnI: "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)" +apply (erule Fin_induct) +apply (simp_all add: Un_cons) +done + +declare Fin_UnI [simp] + + +(*The union of a set of finite sets is finite.*) +lemma Fin_UnionI: "C : Fin(Fin(A)) ==> Union(C) : Fin(A)" +by (erule Fin_induct, simp_all) + +(*Every subset of a finite set is finite.*) +lemma Fin_subset_lemma [rule_format]: "b: Fin(A) ==> \z. z<=b --> z: Fin(A)" +apply (erule Fin_induct) +apply (simp add: subset_empty_iff) +apply (simp add: subset_cons_iff distrib_simps, safe) +apply (erule_tac b = "z" in cons_Diff [THEN subst], simp) +done + +lemma Fin_subset: "[| c<=b; b: Fin(A) |] ==> c: Fin(A)" +by (blast intro: Fin_subset_lemma) + +lemma Fin_IntI1 [intro,simp]: "b: Fin(A) ==> b Int c : Fin(A)" +by (blast intro: Fin_subset) + +lemma Fin_IntI2 [intro,simp]: "c: Fin(A) ==> b Int c : Fin(A)" +by (blast intro: Fin_subset) + +lemma Fin_0_induct_lemma [rule_format]: + "[| c: Fin(A); b: Fin(A); P(b); + !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) + |] ==> c<=b --> P(b-c)" +apply (erule Fin_induct, simp) +apply (subst Diff_cons) +apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset]) +done + +lemma Fin_0_induct: + "[| b: Fin(A); + P(b); + !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) + |] ==> P(0)" +apply (rule Diff_cancel [THEN subst]) +apply (blast intro: Fin_0_induct_lemma) +done + +(*Functions from a finite ordinal*) +lemma nat_fun_subset_Fin: "n: nat ==> n->A <= Fin(nat*A)" +apply (induct_tac "n") +apply (simp add: subset_iff) +apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq]) +apply (fast intro!: Fin.consI) +done + + +(*** Finite function space ***) + +lemma FiniteFun_mono: + "[| A<=C; B<=D |] ==> A -||> B <= C -||> D" +apply (unfold FiniteFun.defs) +apply (rule lfp_mono) +apply (rule FiniteFun.bnd_mono)+ +apply (intro Fin_mono Sigma_mono basic_monos, assumption+) +done + +lemma FiniteFun_mono1: "A<=B ==> A -||> A <= B -||> B" +by (blast dest: FiniteFun_mono) + +lemma FiniteFun_is_fun: "h: A -||>B ==> h: domain(h) -> B" +apply (erule FiniteFun.induct, simp) +apply (simp add: fun_extend3) +done + +lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)" +apply (erule FiniteFun.induct, simp) +apply simp +done + +lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard] + +(*Every subset of a finite function is a finite function.*) +lemma FiniteFun_subset_lemma [rule_format]: + "b: A-||>B ==> ALL z. z<=b --> z: A-||>B" +apply (erule FiniteFun.induct) +apply (simp add: subset_empty_iff FiniteFun.intros) +apply (simp add: subset_cons_iff distrib_simps, safe) +apply (erule_tac b = "z" in cons_Diff [THEN subst]) +apply (drule spec [THEN mp], assumption) +apply (fast intro!: FiniteFun.intros) +done + +lemma FiniteFun_subset: "[| c<=b; b: A-||>B |] ==> c: A-||>B" +by (blast intro: FiniteFun_subset_lemma) + +(** Some further results by Sidi O. Ehmety **) + +lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B" +apply (erule Fin.induct) + apply (simp add: FiniteFun.intros) +apply clarify +apply (case_tac "a:b") + apply (rotate_tac -1) + apply (simp add: cons_absorb) +apply (subgoal_tac "restrict (f,b) : b -||> B") + prefer 2 apply (blast intro: restrict_type2) +apply (subst fun_cons_restrict_eq, assumption) +apply (simp add: restrict_def lam_def) +apply (blast intro: apply_funtype FiniteFun.intros + FiniteFun_mono [THEN [2] rev_subsetD]) +done + +lemma lam_FiniteFun: "A: Fin(X) ==> (lam x:A. b(x)) : A -||> {b(x). x:A}" +by (blast intro: fun_FiniteFunI lam_funtype) + +lemma FiniteFun_Collect_iff: + "f : FiniteFun(A, {y:B. P(y)}) + <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))" +apply auto +apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) +apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) +apply (rule_tac A1="domain(f)" in + subset_refl [THEN [2] FiniteFun_mono, THEN subsetD]) + apply (fast dest: FiniteFun_domain_Fin Fin.dom_subset [THEN subsetD]) +apply (rule fun_FiniteFunI) +apply (erule FiniteFun_domain_Fin) +apply (rule_tac B = "range (f) " in fun_weaken_type) + apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+ +done + +ML +{* +val Fin_intros = thms "Fin.intros"; + +val Fin_mono = thm "Fin_mono"; +val FinD = thm "FinD"; +val Fin_induct = thm "Fin_induct"; +val Fin_UnI = thm "Fin_UnI"; +val Fin_UnionI = thm "Fin_UnionI"; +val Fin_subset = thm "Fin_subset"; +val Fin_IntI1 = thm "Fin_IntI1"; +val Fin_IntI2 = thm "Fin_IntI2"; +val Fin_0_induct = thm "Fin_0_induct"; +val nat_fun_subset_Fin = thm "nat_fun_subset_Fin"; +val FiniteFun_mono = thm "FiniteFun_mono"; +val FiniteFun_mono1 = thm "FiniteFun_mono1"; +val FiniteFun_is_fun = thm "FiniteFun_is_fun"; +val FiniteFun_domain_Fin = thm "FiniteFun_domain_Fin"; +val FiniteFun_apply_type = thm "FiniteFun_apply_type"; +val FiniteFun_subset = thm "FiniteFun_subset"; +val fun_FiniteFunI = thm "fun_FiniteFunI"; +val lam_FiniteFun = thm "lam_FiniteFun"; +val FiniteFun_Collect_iff = thm "FiniteFun_Collect_iff"; +*} + end diff -r d5234c261813 -r 812b00ed1c03 src/ZF/Induct/FoldSet.ML --- a/src/ZF/Induct/FoldSet.ML Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/Induct/FoldSet.ML Fri May 31 15:06:06 2002 +0200 @@ -106,7 +106,7 @@ by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2); by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, Fin_into_Finite RS Finite_imp_cardinal_cons]) 2); -by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2); +by (asm_simp_tac (simpset() addsimps [thm "Fin.consI" RS Fin_into_Finite]) 2); by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A"), ("f1", "f")] (Fin_imp_fold_set RS exE) 1); by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1); @@ -175,7 +175,7 @@ \ ==> : fold_set(cons(c, C), B, f, e) <-> \ \ (EX y. : fold_set(C, B, f, e) & v = f(c, y))"; by Auto_tac; -by (forward_tac [inst "a" "c" Fin.consI RS FinD RS fold_set_mono RS subsetD] 1); +by (forward_tac [inst "a" "c" (thm"Fin.consI") RS FinD RS fold_set_mono RS subsetD] 1); by (assume_tac 1); by (assume_tac 1); by (forward_tac [FinD RS fold_set_mono RS subsetD] 2); diff -r d5234c261813 -r 812b00ed1c03 src/ZF/Induct/FoldSet.thy --- a/src/ZF/Induct/FoldSet.thy Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/Induct/FoldSet.thy Fri May 31 15:06:06 2002 +0200 @@ -18,7 +18,7 @@ emptyI "e:B ==> <0, e>:fold_set(A, B, f,e)" consI "[| x:A; x ~:C; : fold_set(A, B,f,e); f(x,y):B |] ==> :fold_set(A, B, f, e)" - type_intrs "Fin.intrs" + type_intrs "Fin_intros" constdefs diff -r d5234c261813 -r 812b00ed1c03 src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/Induct/Multiset.ML Fri May 31 15:06:06 2002 +0200 @@ -104,7 +104,7 @@ (* the empty multiset is 0 *) Goal "multiset(0)"; -by (auto_tac (claset() addIs FiniteFun.intrs, +by (auto_tac (claset() addIs (thms"FiniteFun.intros"), simpset() addsimps [multiset_iff_Mult_mset_of])); qed "multiset_0"; Addsimps [multiset_0]; diff -r d5234c261813 -r 812b00ed1c03 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/IsaMakefile Fri May 31 15:06:06 2002 +0200 @@ -31,7 +31,7 @@ $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \ ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \ - Datatype.ML Datatype.thy Epsilon.thy Finite.ML Finite.thy \ + Datatype.ML Datatype.thy Epsilon.thy Finite.thy \ Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy \ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ diff -r d5234c261813 -r 812b00ed1c03 src/ZF/UNITY/Guar.ML --- a/src/ZF/UNITY/Guar.ML Fri May 31 12:27:24 2002 +0200 +++ b/src/ZF/UNITY/Guar.ML Fri May 31 15:06:06 2002 +0200 @@ -417,7 +417,7 @@ by (Clarify_tac 1); by (subgoal_tac "F component_of (JN F:FF. F)" 1); by (dres_inst_tac [("X", "X")] component_of_wg 1); -by (force_tac (claset() addSDs [Fin.dom_subset RS subsetD RS PowD], +by (force_tac (claset() addSDs [thm"Fin.dom_subset" RS subsetD RS PowD], simpset()) 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def]))); by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);