src/HOL/Library/Library.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16109 e8c169d6f191
child 16908 d374530bfaaa
permissions -rw-r--r--
Constant "If" is now local
wenzelm@10253
     1
(*<*)
nipkow@15131
     2
theory Library
nipkow@15140
     3
imports
nipkow@15131
     4
  Accessible_Part
nipkow@15131
     5
  Continuity
berghofe@15324
     6
  EfficientNat
nipkow@15131
     7
  FuncSet
nipkow@15131
     8
  Multiset
nipkow@15131
     9
  NatPair
nipkow@15131
    10
  Nat_Infinity
nipkow@15131
    11
  Nested_Environment
nipkow@15470
    12
  OptionalSugar
nipkow@15131
    13
  Permutation
nipkow@15131
    14
  Primes
nipkow@15131
    15
  Quotient
nipkow@15131
    16
  While_Combinator
nipkow@15131
    17
  Word
nipkow@15131
    18
  Zorn
obua@16109
    19
  (*List_Prefix*)
nipkow@15731
    20
  Char_ord
nipkow@15731
    21
  List_lexord
nipkow@15131
    22
begin
wenzelm@10253
    23
end
wenzelm@10253
    24
(*>*)