src/ZF/AC/AC2_AC6.ML
changeset 2717 b29c45ef3d86
parent 2496 40efb87985b5
child 4091 771b1f6422a8
equal deleted inserted replaced
2716:9e11a914156a 2717:b29c45ef3d86
    76 val lemma = result();
    76 val lemma = result();
    77 
    77 
    78 goalw thy AC_defs "!!Z. AC1 ==> AC4";
    78 goalw thy AC_defs "!!Z. AC1 ==> AC4";
    79 by (REPEAT (resolve_tac [allI, impI] 1));
    79 by (REPEAT (resolve_tac [allI, impI] 1));
    80 by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
    80 by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
    81 by (fast_tac (!claset addSIs [lam_type] addSEs [apply_type]) 1);
    81 by (best_tac (!claset addSIs [lam_type] addSEs [apply_type]) 1);
    82 qed "AC1_AC4";
    82 qed "AC1_AC4";
    83 
    83 
    84 
    84 
    85 (* ********************************************************************** *)
    85 (* ********************************************************************** *)
    86 (* AC4 ==> AC3                                                            *)
    86 (* AC4 ==> AC3                                                            *)