src/HOL/Library/Library.thy
author obua
Mon Aug 01 11:39:33 2005 +0200 (2005-08-01)
changeset 16966 37e34f315057
parent 16908 d374530bfaaa
child 17516 45164074dad4
permissions -rw-r--r--
1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML
     1 (*<*)
     2 theory Library
     3 imports
     4   Accessible_Part
     5   BigO
     6   Continuity
     7   EfficientNat
     8   FuncSet
     9   Multiset
    10   NatPair
    11   Nat_Infinity
    12   Nested_Environment
    13   OptionalSugar
    14   Permutation
    15   Primes
    16   Quotient
    17   While_Combinator
    18   Word
    19   Zorn
    20   Char_ord
    21 begin
    22 end
    23 (*>*)