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
     1 (*  Title:      HOL/SetInterval.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin
     4     Copyright   2002  TU Muenchen
     5 *)
     6 
     7 (* Legacy ML bindings *)
     8 
     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";
    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";