| changeset 6498 | 1ebbe18fe236 |
| parent 3458 | 5ff4bfab859c |
| 6497:120ca2bb27e1 | 6498:1ebbe18fe236 |
|---|---|
7 signature Thms_sig = |
7 signature Thms_sig = |
8 sig |
8 sig |
9 val WF_INDUCTION_THM:thm |
9 val WF_INDUCTION_THM:thm |
10 val WFREC_COROLLARY :thm |
10 val WFREC_COROLLARY :thm |
11 val CUT_DEF :thm |
11 val CUT_DEF :thm |
12 val CUT_LEMMA :thm |
|
13 val SELECT_AX :thm |
12 val SELECT_AX :thm |
14 |
13 |
15 val LET_CONG :thm |
14 val LET_CONG :thm |
16 |
15 |
17 val eqT :thm |
16 val eqT :thm |