equal
deleted
inserted
replaced
1 (* Title: ZF/Constructible/Rank_Separation.thy |
1 (* Title: ZF/Constructible/Rank_Separation.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 *) |
3 *) |
5 |
4 |
6 header {*Separation for Facts About Order Types, Rank Functions and |
5 header {*Separation for Facts About Order Types, Rank Functions and |
7 Well-Founded Relations*} |
6 Well-Founded Relations*} |
115 such as intersection, Cartesian Product and image.*} |
114 such as intersection, Cartesian Product and image.*} |
116 |
115 |
117 lemma M_ordertype_axioms_L: "M_ordertype_axioms(L)" |
116 lemma M_ordertype_axioms_L: "M_ordertype_axioms(L)" |
118 apply (rule M_ordertype_axioms.intro) |
117 apply (rule M_ordertype_axioms.intro) |
119 apply (assumption | rule well_ord_iso_separation |
118 apply (assumption | rule well_ord_iso_separation |
120 obase_separation obase_equals_separation |
119 obase_separation obase_equals_separation |
121 omap_replacement)+ |
120 omap_replacement)+ |
122 done |
121 done |
123 |
122 |
124 theorem M_ordertype_L: "PROP M_ordertype(L)" |
123 theorem M_ordertype_L: "PROP M_ordertype(L)" |
125 apply (rule M_ordertype.intro) |
124 apply (rule M_ordertype.intro) |
126 apply (rule M_basic_L) |
125 apply (rule M_basic_L) |