equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
4 *) |
5 |
5 |
6 header {* The ZF Axioms (Except Separation) in L *} |
6 header {* The ZF Axioms (Except Separation) in L *} |
7 |
7 |
8 theory L_axioms = Formula + Relative + Reflection + MetaExists: |
8 theory L_axioms imports Formula Relative Reflection MetaExists begin |
9 |
9 |
10 text {* The class L satisfies the premises of locale @{text M_trivial} *} |
10 text {* The class L satisfies the premises of locale @{text M_trivial} *} |
11 |
11 |
12 lemma transL: "[| y\<in>x; L(x) |] ==> L(y)" |
12 lemma transL: "[| y\<in>x; L(x) |] ==> L(y)" |
13 apply (insert Transset_Lset) |
13 apply (insert Transset_Lset) |