|
8956
|
1 |
(* Title: HOL/SetInterval.ML
|
|
|
2 |
ID: $Id$
|
|
13735
|
3 |
Author: Clemens Ballarin
|
|
|
4 |
Copyright 2002 TU Muenchen
|
|
8956
|
5 |
*)
|
|
|
6 |
|
|
13735
|
7 |
(* Legacy ML bindings *)
|
|
8956
|
8 |
|
|
13735
|
9 |
val Compl_atLeast = thm "Compl_atLeast";
|
|
|
10 |
val Compl_atMost = thm "Compl_atMost";
|
|
|
11 |
val Compl_greaterThan = thm "Compl_greaterThan";
|
|
|
12 |
val Compl_lessThan = thm "Compl_lessThan";
|
|
|
13 |
val INT_greaterThan_UNIV = thm "INT_greaterThan_UNIV";
|
|
|
14 |
val UN_atLeast_UNIV = thm "UN_atLeast_UNIV";
|
|
|
15 |
val UN_atMost_UNIV = thm "UN_atMost_UNIV";
|
|
|
16 |
val UN_lessThan_UNIV = thm "UN_lessThan_UNIV";
|
|
|
17 |
val atLeastAtMost_def = thm "atLeastAtMost_def";
|
|
|
18 |
val atLeastAtMost_iff = thm "atLeastAtMost_iff";
|
|
|
19 |
val atLeastLessThan_def = thm "atLeastLessThan_def";
|
|
|
20 |
val atLeastLessThan_iff = thm "atLeastLessThan_iff";
|
|
|
21 |
val atLeast_0 = thm "atLeast_0";
|
|
|
22 |
val atLeast_Suc = thm "atLeast_Suc";
|
|
|
23 |
val atLeast_def = thm "atLeast_def";
|
|
|
24 |
val atLeast_iff = thm "atLeast_iff";
|
|
|
25 |
val atMost_0 = thm "atMost_0";
|
|
|
26 |
val atMost_Int_atLeast = thm "atMost_Int_atLeast";
|
|
|
27 |
val atMost_Suc = thm "atMost_Suc";
|
|
|
28 |
val atMost_def = thm "atMost_def";
|
|
|
29 |
val atMost_iff = thm "atMost_iff";
|
|
|
30 |
val greaterThanAtMost_def = thm "greaterThanAtMost_def";
|
|
|
31 |
val greaterThanAtMost_iff = thm "greaterThanAtMost_iff";
|
|
|
32 |
val greaterThanLessThan_def = thm "greaterThanLessThan_def";
|
|
|
33 |
val greaterThanLessThan_iff = thm "greaterThanLessThan_iff";
|
|
|
34 |
val greaterThan_0 = thm "greaterThan_0";
|
|
|
35 |
val greaterThan_Suc = thm "greaterThan_Suc";
|
|
|
36 |
val greaterThan_def = thm "greaterThan_def";
|
|
|
37 |
val greaterThan_iff = thm "greaterThan_iff";
|
|
|
38 |
val ivl_disj_int = thms "ivl_disj_int";
|
|
|
39 |
val ivl_disj_int_one = thms "ivl_disj_int_one";
|
|
|
40 |
val ivl_disj_int_singleton = thms "ivl_disj_int_singleton";
|
|
|
41 |
val ivl_disj_int_two = thms "ivl_disj_int_two";
|
|
|
42 |
val ivl_disj_un = thms "ivl_disj_un";
|
|
|
43 |
val ivl_disj_un_one = thms "ivl_disj_un_one";
|
|
|
44 |
val ivl_disj_un_singleton = thms "ivl_disj_un_singleton";
|
|
|
45 |
val ivl_disj_un_two = thms "ivl_disj_un_two";
|
|
|
46 |
val lessThan_0 = thm "lessThan_0";
|
|
|
47 |
val lessThan_Suc = thm "lessThan_Suc";
|
|
|
48 |
val lessThan_Suc_atMost = thm "lessThan_Suc_atMost";
|
|
|
49 |
val lessThan_def = thm "lessThan_def";
|
|
|
50 |
val lessThan_iff = thm "lessThan_iff";
|
|
|
51 |
val single_Diff_lessThan = thm "single_Diff_lessThan";
|
|
14485
|
52 |
|
|
|
53 |
val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
|
|
|
54 |
val finite_atMost = thm "finite_atMost";
|
|
|
55 |
val finite_lessThan = thm "finite_lessThan";
|