equal
deleted
inserted
replaced
18 |
18 |
19 val AC_cs = OrdQuant_cs; |
19 val AC_cs = OrdQuant_cs; |
20 val AC_ss = OrdQuant_ss; |
20 val AC_ss = OrdQuant_ss; |
21 |
21 |
22 (* ******************************************** *) |
22 (* ******************************************** *) |
|
23 |
|
24 val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel; |
23 |
25 |
24 (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) |
26 (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) |
25 |
27 |
26 (* lemma for nat_le_imp_lepoll *) |
28 (* lemma for nat_le_imp_lepoll *) |
27 val [prem] = goalw Cardinal.thy [lepoll_def] |
29 val [prem] = goalw Cardinal.thy [lepoll_def] |