| author | paulson |
| Wed, 21 Dec 2005 12:02:57 +0100 | |
| changeset 18447 | da548623916a |
| parent 13704 | 854501b1e957 |
| permissions | -rw-r--r-- |
| 12691 | 1 |
|
2 |
(* legacy ML bindings *) |
|
3 |
||
4 |
val converse_rtranclE = thm "converse_rtranclE"; |
|
5 |
val converse_rtranclE2 = thm "converse_rtranclE2"; |
|
6 |
val converse_rtrancl_induct = thm "converse_rtrancl_induct"; |
|
7 |
val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2"; |
|
8 |
val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl"; |
|
9 |
val converse_trancl_induct = thm "converse_trancl_induct"; |
|
10 |
val irrefl_tranclI = thm "irrefl_tranclI"; |
|
11 |
val irrefl_trancl_rD = thm "irrefl_trancl_rD"; |
|
12 |
val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq"; |
|
13 |
val r_into_rtrancl = thm "r_into_rtrancl"; |
|
14 |
val r_into_trancl = thm "r_into_trancl"; |
|
15 |
val rtranclE = thm "rtranclE"; |
|
16 |
val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl"; |
|
17 |
val rtrancl_converse = thm "rtrancl_converse"; |
|
18 |
val rtrancl_converseD = thm "rtrancl_converseD"; |
|
19 |
val rtrancl_converseI = thm "rtrancl_converseI"; |
|
20 |
val rtrancl_idemp = thm "rtrancl_idemp"; |
|
21 |
val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp"; |
|
22 |
val rtrancl_induct = thm "rtrancl_induct"; |
|
23 |
val rtrancl_induct2 = thm "rtrancl_induct2"; |
|
24 |
val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl"; |
|
25 |
val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1"; |
|
26 |
val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2"; |
|
27 |
val rtrancl_mono = thm "rtrancl_mono"; |
|
28 |
val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id"; |
|
29 |
val rtrancl_refl = thm "rtrancl_refl"; |
|
30 |
val rtrancl_reflcl = thm "rtrancl_reflcl"; |
|
31 |
val rtrancl_subset = thm "rtrancl_subset"; |
|
32 |
val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl"; |
|
33 |
val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; |
|
34 |
val rtrancl_trans = thm "rtrancl_trans"; |
|
35 |
val tranclD = thm "tranclD"; |
|
36 |
val tranclE = thm "tranclE"; |
|
37 |
val trancl_converse = thm "trancl_converse"; |
|
38 |
val trancl_converseD = thm "trancl_converseD"; |
|
39 |
val trancl_converseI = thm "trancl_converseI"; |
|
40 |
val trancl_induct = thm "trancl_induct"; |
|
41 |
val trancl_insert = thm "trancl_insert"; |
|
42 |
val trancl_into_rtrancl = thm "trancl_into_rtrancl"; |
|
|
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12691
diff
changeset
|
43 |
val trancl_into_trancl = thm "trancl_into_trancl"; |
| 12691 | 44 |
val trancl_into_trancl2 = thm "trancl_into_trancl2"; |
45 |
val trancl_mono = thm "trancl_mono"; |
|
46 |
val trancl_subset_Sigma = thm "trancl_subset_Sigma"; |
|
47 |
val trancl_trans = thm "trancl_trans"; |
|
48 |
val trancl_trans_induct = thm "trancl_trans_induct"; |
|
49 |
val trans_rtrancl = thm "trans_rtrancl"; |
|
50 |
val trans_trancl = thm "trans_trancl"; |