src/HOL/Library/Library.thy
author nipkow
Wed Jan 26 16:39:44 2005 +0100 (2005-01-26)
changeset 15470 7e12ad2f6672
parent 15324 c27165172e30
child 15731 29ae73d8a84e
permissions -rw-r--r--
added OptionalSugar
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
  List_Prefix
nipkow@15131
     9
  Multiset
nipkow@15131
    10
  NatPair
nipkow@15131
    11
  Nat_Infinity
nipkow@15131
    12
  Nested_Environment
nipkow@15470
    13
  OptionalSugar
nipkow@15131
    14
  Permutation
nipkow@15131
    15
  Primes
nipkow@15131
    16
  Quotient
nipkow@15131
    17
  While_Combinator
nipkow@15131
    18
  Word
nipkow@15131
    19
  Zorn
nipkow@15131
    20
begin
wenzelm@10253
    21
end
wenzelm@10253
    22
(*>*)