src/HOL/Library/Library.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 65050 4538153bcc5c
child 65417 fc41a5650fb1
permissions -rw-r--r--
tuned proofs;
wenzelm@10253
     1
(*<*)
nipkow@15131
     2
theory Library
nipkow@15140
     3
imports
haftmann@51161
     4
  AList
avigad@16908
     5
  BigO
huffman@29994
     6
  Bit
traytel@56942
     7
  BNF_Axiomatization
blanchet@62692
     8
  BNF_Corec
kleing@24332
     9
  Boolean_Algebra
Andreas@61766
    10
  Bourbaki_Witt_Fixpoint
wenzelm@21256
    11
  Char_ord
Andreas@58626
    12
  Code_Test
haftmann@63377
    13
  Combine_PER
Andreas@62652
    14
  Complete_Partial_Order2
haftmann@26170
    15
  Countable
hoelzl@62373
    16
  Countable_Complete_Lattices
blanchet@55075
    17
  Countable_Set_Type
haftmann@48427
    18
  Debug
immler@50087
    19
  Diagonal_Subsequence
hoelzl@60727
    20
  Disjoint_Sets
haftmann@48283
    21
  Dlist
wenzelm@51542
    22
  Extended
wenzelm@51542
    23
  Extended_Nat
hoelzl@62375
    24
  Extended_Nonnegative_Real
wenzelm@51542
    25
  Extended_Real
lars@63885
    26
  Finite_Map
haftmann@28952
    27
  Float
chaieb@29688
    28
  Formal_Power_Series
chaieb@31761
    29
  Fraction_Field
kuncar@53953
    30
  FSet
wenzelm@21256
    31
  FuncSet
haftmann@48188
    32
  Function_Division
haftmann@51263
    33
  Function_Growth
nipkow@29879
    34
  Fundamental_Theorem_Algebra
haftmann@58196
    35
  Fun_Lexorder
haftmann@58197
    36
  Groups_Big_Fun
hoelzl@37665
    37
  Indicator_Function
huffman@27475
    38
  Infinite_Set
haftmann@51161
    39
  IArray
haftmann@35032
    40
  Lattice_Algebras
haftmann@30326
    41
  Lattice_Syntax
Andreas@57998
    42
  Lattice_Constructions
hoelzl@58627
    43
  Linear_Temporal_Logic_on_Streams
wenzelm@26173
    44
  ListVector
wenzelm@58810
    45
  Lub_Glb
haftmann@29708
    46
  Mapping
krauss@37790
    47
  Monad_Syntax
haftmann@58199
    48
  More_List
blanchet@59813
    49
  Multiset_Order
eberlm@63965
    50
  Multiset_Permutations
haftmann@64588
    51
  Nonpos_Ints
kleing@24332
    52
  Numeral_Type
lammich@61178
    53
  Omega_Words_Fun
nipkow@15470
    54
  OptionalSugar
haftmann@26232
    55
  Option_ord
hoelzl@56020
    56
  Order_Continuity
haftmann@48427
    57
  Parallel
haftmann@64588
    58
  Periodic_Fun
haftmann@63375
    59
  Perm
nipkow@15131
    60
  Permutation
huffman@44227
    61
  Permutations
huffman@29987
    62
  Polynomial
eberlm@63317
    63
  Polynomial_FPS
haftmann@31060
    64
  Preorder
hoelzl@63972
    65
  Product_Plus
lp15@60162
    66
  Quadratic_Discriminant
kaliszyk@35222
    67
  Quotient_List
kaliszyk@35222
    68
  Quotient_Option
kaliszyk@35222
    69
  Quotient_Product
haftmann@45074
    70
  Quotient_Set
kaliszyk@35222
    71
  Quotient_Sum
kaliszyk@35222
    72
  Quotient_Syntax
wenzelm@35100
    73
  Quotient_Type
krauss@21635
    74
  Ramsey
haftmann@29650
    75
  Reflection
haftmann@64588
    76
  Rewrite
haftmann@44818
    77
  Saturated
haftmann@38622
    78
  Set_Algebras
wenzelm@21256
    79
  State_Monad
hoelzl@63071
    80
  Stirling
hoelzl@58607
    81
  Stream
haftmann@51161
    82
  Sublist
wenzelm@41474
    83
  Sum_of_Squares
bulwahn@33649
    84
  Transitive_Closure_Table
nipkow@59928
    85
  Tree_Multiset
wenzelm@63762
    86
  Type_Length
nipkow@15131
    87
  While_Combinator
nipkow@15131
    88
begin
wenzelm@10253
    89
end
wenzelm@10253
    90
(*>*)