src/ZF/AC/DC.thy

 done
 
 lemma range_subset_domain: 
       "[| R \<subseteq> X*X;   !!g. g \<in> X ==> \<exists>u. <g,u> \<in> R |] 
        ==> range(R) \<subseteq> domain(R)"
-by (blast ); 
+by blast 
 
 lemma cons_fun_type: "g \<in> n->X ==> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)"
 apply (unfold succ_def)
 apply (fast intro!: fun_extend elim!: mem_irrefl)
 done

   apply (blast intro: fun_weaken_type)
  apply (erule ltD) 
 (** LEVEL 11: last subgoal **)
 apply (subst DC0_imp.lemma3, assumption+) 
   apply (fast elim!: fun_weaken_type)
- apply (erule ltD, force) 
+ apply (erule ltD) 
+apply (force simp add: lt_def) 
 done
 
 
 (* ************************************************************************
    DC(omega) ==> DC                                                       

 apply (blast intro: Ord_in_Ord, auto) 
 apply (atomize, blast dest: not_sym) 
 done
 
 lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
-by (fast elim!: image_fun [THEN ssubst]);
+by (fast elim!: image_fun [THEN ssubst])
 
 theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
 apply (unfold DC_def WO3_def)
 apply (rule allI)
 apply (case_tac "A \<prec> Hartog (A)")