# HG changeset patch # User lcp # Date 785669021 -3600 # Node ID 436019ca97d7b22f39f813242aea7d57c7410cf1 # Parent a8d1758bb1131e1feffddf803b36fd6e9073150e cons_fun_eq: modified strange uses of classical reasoner diff -r a8d1758bb113 -r 436019ca97d7 src/ZF/func.ML --- a/src/ZF/func.ML Thu Nov 24 00:33:13 1994 +0100 +++ b/src/ZF/func.ML Thu Nov 24 10:23:41 1994 +0100 @@ -380,12 +380,13 @@ (*For Finite.ML. Inclusion of right into left is easy*) goal ZF.thy "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(, f)})"; -by (safe_tac (eq_cs addSEs [fun_extend3])); +by (rtac equalityI 1); +by (safe_tac (ZF_cs addSEs [fun_extend3])); (*Inclusion of left into right*) by (subgoal_tac "restrict(x, A) : A -> B" 1); by (fast_tac (ZF_cs addEs [restrict_type2]) 2); by (rtac UN_I 1 THEN assume_tac 1); -by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1); +by (rtac (apply_funtype RS UN_I) 1 THEN REPEAT (ares_tac [consI1] 1)); by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1); by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1)); by (etac consE 1);