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