--- a/src/ZF/AC/AC18_AC19.thy Wed Jul 24 00:12:50 2002 +0200
+++ b/src/ZF/AC/AC18_AC19.thy Wed Jul 24 00:13:41 2002 +0200
@@ -34,8 +34,9 @@
apply (simp, fast elim!: not_emptyE dest: apply_type [OF _ RepFunI])
done
-lemma AC1_AC18: "AC1 ==> AC18"
-apply (unfold AC1_def AC18_def)
+lemma AC1_AC18: "AC1 ==> PROP AC18"
+apply (unfold AC1_def)
+apply (rule AC18.intro [OF AC18_axioms.intro])
apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
done
@@ -43,16 +44,11 @@
(* AC18 ==> AC19 *)
(* ********************************************************************** *)
-text{*Hard to express because of the need for meta-quantifiers in AC18*}
-lemma "AC18 ==> AC19"
-proof -
- assume ac18 [unfolded AC18_def, norm_hhf]: AC18
- show AC19
- apply (unfold AC18_def AC19_def)
- apply (intro allI impI)
- apply (rule ac18 [of _ "%x. x", THEN mp], blast)
- done
-qed
+theorem (in AC18) AC19
+apply (unfold AC19_def)
+apply (intro allI impI)
+apply (rule AC18 [of _ "%x. x", THEN mp], blast)
+done
(* ********************************************************************** *)
(* AC19 ==> AC1 *)