equal
deleted
inserted
replaced
1 (* Title: ZF/Constructible/L_axioms.thy |
1 (* Title: ZF/Constructible/L_axioms.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2002 University of Cambridge |
|
5 *) |
4 *) |
6 |
5 |
7 header {* The ZF Axioms (Except Separation) in L *} |
6 header {* The ZF Axioms (Except Separation) in L *} |
8 |
7 |
9 theory L_axioms = Formula + Relative + Reflection + MetaExists: |
8 theory L_axioms = Formula + Relative + Reflection + MetaExists: |