src/HOL/Library/Library.thy
author krauss
Fri, 05 May 2006 17:17:21 +0200
changeset 19564 d3e2f532459a
parent 19469 958d2f2dd8d4
child 19605 67e6b4759b37
permissions -rw-r--r--
First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     1
(*<*)
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
     2
theory Library
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     3
imports
16908
d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents: 16109
diff changeset
     4
  BigO
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
     5
  Continuity
15324
c27165172e30 Added EfficientNat
berghofe
parents: 15140
diff changeset
     6
  EfficientNat
17633
7daaa7fe9c96 Added ExecutableSet.
berghofe
parents: 17516
diff changeset
     7
  ExecutableSet
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
     8
  FuncSet
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
     9
  Multiset
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    10
  NatPair
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    11
  Nat_Infinity
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    12
  Nested_Environment
15470
7e12ad2f6672 added OptionalSugar
nipkow
parents: 15324
diff changeset
    13
  OptionalSugar
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    14
  Permutation
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    15
  Primes
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    16
  Quotient
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    17
  While_Combinator
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    18
  Word
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    19
  Zorn
15731
29ae73d8a84e Removed dir Orderings in Library
nipkow
parents: 15470
diff changeset
    20
  Char_ord
17516
45164074dad4 added Commutative_Ring (from Main HOL);
wenzelm
parents: 16966
diff changeset
    21
  Commutative_Ring
18397
2d94eb7ff17f added HOL/Library/Coinductive_List.thy;
wenzelm
parents: 17633
diff changeset
    22
  Coinductive_List
19234
054332e39e0a Added Library/AssocList.thy
schirmer
parents: 19106
diff changeset
    23
  AssocList
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    24
begin
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    25
end
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    26
(*>*)