src/HOL/Library/Library.thy
author haftmann
Sat, 06 Sep 2014 20:12:34 +0200
changeset 58196 1b3fbfb85980
parent 58110 019c0211ed1f
child 58197 4fd7f47ead6c
permissions -rw-r--r--
theory about lexicographic ordering on functions
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
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset
     4
  AList
16908
d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents: 16109
diff changeset
     5
  BigO
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents: 29993
diff changeset
     6
  Bit
56942
5fff4dc31d34 bnf_decl -> bnf_axiomatization
traytel
parents: 56415
diff changeset
     7
  BNF_Axiomatization
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24281
diff changeset
     8
  Boolean_Algebra
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset
     9
  Char_ord
29026
5fbaa05f637f moved ContNotDenum into Library
nipkow
parents: 28952
diff changeset
    10
  ContNotDenum
36648
43b66dcd9266 Add Convex to Library build
hoelzl
parents: 36147
diff changeset
    11
  Convex
26170
66e6b967ccf1 added theories for imperative HOL
haftmann
parents: 26157
diff changeset
    12
  Countable
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55018
diff changeset
    13
  Countable_Set_Type
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset
    14
  Debug
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 48742
diff changeset
    15
  Diagonal_Subsequence
48283
8a1ef12f7e6d explicitly import Dlist theory into library
haftmann
parents: 48188
diff changeset
    16
  Dlist
51542
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset
    17
  Extended
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset
    18
  Extended_Nat
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset
    19
  Extended_Real
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents: 47232
diff changeset
    20
  FinFun
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28668
diff changeset
    21
  Float
29688
6ed9ac8410d8 Added Formal_Power_Series in imports
chaieb
parents: 29650
diff changeset
    22
  Formal_Power_Series
31761
3585bebe49a8 Added Library/Fraction_Field.thy: The fraction field of any integral
chaieb
parents: 31379
diff changeset
    23
  Fraction_Field
53953
2f103a894ebe new theory of finite sets as a subtype
kuncar
parents: 52192
diff changeset
    24
  FSet
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset
    25
  FuncSet
48188
dcfe2c92fc7c Stub theory for division on functionals.
haftmann
parents: 48028
diff changeset
    26
  Function_Division
51263
31e786e0e6a7 turned example into library for comparing growth of functions
haftmann
parents: 51174
diff changeset
    27
  Function_Growth
29879
4425849f5db7 Moved FTA into Lib and cleaned it up a little.
nipkow
parents: 29847
diff changeset
    28
  Fundamental_Theorem_Algebra
58196
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents: 58110
diff changeset
    29
  Fun_Lexorder
37665
579258a77fec Add theory for indicator function.
hoelzl
parents: 37023
diff changeset
    30
  Indicator_Function
27475
61b979a2c820 add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
huffman
parents: 27368
diff changeset
    31
  Infinite_Set
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents: 29987
diff changeset
    32
  Inner_Product
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset
    33
  IArray
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 34020
diff changeset
    34
  Lattice_Algebras
30326
a01b2de0e3e1 constructive version of Cantor's first diagonalization argument
haftmann
parents: 30261
diff changeset
    35
  Lattice_Syntax
57998
8b7508f848ef rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents: 57250
diff changeset
    36
  Lattice_Constructions
26173
5cac519abe4e renamed ListSpace to ListVector;
wenzelm
parents: 26170
diff changeset
    37
  ListVector
56415
f61a0f7cbde5 proper inclusion into library
haftmann
parents: 56020
diff changeset
    38
  Lubs_Glbs
29708
e40b70d38909 added Mapping.thy to Library
haftmann
parents: 29688
diff changeset
    39
  Mapping
37790
7fea92005066 uniform do notation for monads
krauss
parents: 37789
diff changeset
    40
  Monad_Syntax
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    41
  Multiset
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24281
diff changeset
    42
  Numeral_Type
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56942
diff changeset
    43
  NthRoot_Limits
15470
7e12ad2f6672 added OptionalSugar
nipkow
parents: 15324
diff changeset
    44
  OptionalSugar
26232
075264a0a4bc canonical order on option type
haftmann
parents: 26192
diff changeset
    45
  Option_ord
56020
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55159
diff changeset
    46
  Order_Continuity
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset
    47
  Parallel
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    48
  Permutation
44227
78e033e8ba05 get Library/Permutations.thy compiled and working again
huffman
parents: 44014
diff changeset
    49
  Permutations
29985
57975b45ab70 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents: 29879
diff changeset
    50
  Poly_Deriv
29987
391dcbd7e4dd move Polynomial.thy to Library
huffman
parents: 29986
diff changeset
    51
  Polynomial
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents: 30326
diff changeset
    52
  Preorder
30019
a2f19e0a28b2 add theory of products as real vector spaces to Library
huffman
parents: 30018
diff changeset
    53
  Product_Vector
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset
    54
  Quotient_List
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset
    55
  Quotient_Option
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset
    56
  Quotient_Product
45074
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 44897
diff changeset
    57
  Quotient_Set
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset
    58
  Quotient_Sum
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset
    59
  Quotient_Syntax
35100
53754ec7360b renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents: 35091
diff changeset
    60
  Quotient_Type
21635
32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents: 21256
diff changeset
    61
  Ramsey
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 29504
diff changeset
    62
  Reflection
44818
27ba81ad0890 theory of saturated naturals contributed by Peter Gammie
haftmann
parents: 44561
diff changeset
    63
  Saturated
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 37818
diff changeset
    64
  Set_Algebras
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset
    65
  State_Monad
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset
    66
  Sublist
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 40673
diff changeset
    67
  Sum_of_Squares
33649
854173fcd21c added a tabled implementation of the reflexive transitive closure
bulwahn
parents: 33356
diff changeset
    68
  Transitive_Closure_Table
57250
cddaf5b93728 new theory of binary trees
nipkow
parents: 57112
diff changeset
    69
  Tree
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    70
  While_Combinator
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset
    71
begin
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    72
end
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    73
(*>*)