|
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_def = thm "trancl_def";
|
|
|
41 |
val trancl_induct = thm "trancl_induct";
|
|
|
42 |
val trancl_insert = thm "trancl_insert";
|
|
|
43 |
val trancl_into_rtrancl = thm "trancl_into_rtrancl";
|
|
|
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";
|