src/HOL/Library/Library.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 14706 71590b7733b7
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
wenzelm@10253
     1
(*<*)
nipkow@15131
     2
theory Library
nipkow@15131
     3
import
nipkow@15131
     4
  Accessible_Part
nipkow@15131
     5
  Continuity
nipkow@15131
     6
  FuncSet
nipkow@15131
     7
  List_Prefix
nipkow@15131
     8
  Multiset
nipkow@15131
     9
  NatPair
nipkow@15131
    10
  Nat_Infinity
nipkow@15131
    11
  Nested_Environment
nipkow@15131
    12
  Permutation
nipkow@15131
    13
  Primes
nipkow@15131
    14
  Quotient
nipkow@15131
    15
  While_Combinator
nipkow@15131
    16
  Word
nipkow@15131
    17
  Zorn
nipkow@15131
    18
begin
wenzelm@10253
    19
end
wenzelm@10253
    20
(*>*)