equal
deleted
inserted
replaced
14 theory upair |
14 theory upair |
15 imports ZF_Base |
15 imports ZF_Base |
16 keywords "print_tcset" :: diag |
16 keywords "print_tcset" :: diag |
17 begin |
17 begin |
18 |
18 |
19 ML_file "Tools/typechk.ML" |
19 ML_file \<open>Tools/typechk.ML\<close> |
20 |
20 |
21 lemma atomize_ball [symmetric, rulify]: |
21 lemma atomize_ball [symmetric, rulify]: |
22 "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" |
22 "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" |
23 by (simp add: Ball_def atomize_all atomize_imp) |
23 by (simp add: Ball_def atomize_all atomize_imp) |
24 |
24 |