Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Library.thy
author Lars Hupel <lars.hupel@mytum.de>
Thu, 15 Sep 2016 22:41:05 +0200
changeset 63885 a6cd18af8bf9
parent 63762 6920b1885eff
child 63965 d510b816ea41
permissions -rw-r--r--
new type for finite maps; use it in HOL-Probability
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
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents: 62652
diff changeset 
     8
 
  BNF_Corec
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24281
diff changeset 
     9
 
  Boolean_Algebra
61766
507b39df1a57 add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents: 61178
diff changeset 
    10
 
  Bourbaki_Witt_Fixpoint
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset 
    11
 
  Char_ord
58626
6c473ed0ac70 move Code_Test to HOL/Library;
Andreas Lochbihler
parents: 58607
diff changeset 
    12
 
  Code_Test
63464
9d4dbb7a548a more standard name;
wenzelm
parents: 63377
diff changeset 
    13
 
  Continuum_Not_Denumerable
36648
43b66dcd9266 Add Convex to Library build
hoelzl
parents: 36147
diff changeset 
    14
 
  Convex
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents: 63375
diff changeset 
    15
 
  Combine_PER
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents: 62375
diff changeset 
    16
 
  Complete_Partial_Order2
26170
66e6b967ccf1 added theories for imperative HOL
haftmann
parents: 26157
diff changeset 
    17
 
  Countable
62373
ea7a442e9a56 add countable complete lattices
hoelzl
parents: 62352
diff changeset 
    18
 
  Countable_Complete_Lattices
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55018
diff changeset 
    19
 
  Countable_Set_Type
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset 
    20
 
  Debug
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 48742
diff changeset 
    21
 
  Diagonal_Subsequence
60727
53697011b03a move disjoint sets to their own theory
hoelzl
parents: 60162
diff changeset 
    22
 
  Disjoint_Sets
48283
8a1ef12f7e6d explicitly import Dlist theory into library
haftmann
parents: 48188
diff changeset 
    23
 
  Dlist
51542
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    24
 
  Extended
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    25
 
  Extended_Nat
62375
670063003ad3 add extended nonnegative real numbers
hoelzl
parents: 62373
diff changeset 
    26
 
  Extended_Nonnegative_Real
51542
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    27
 
  Extended_Real
48028
a5377f6d9f14 move FinFuns from AFP to repository
Andreas Lochbihler
parents: 47232
diff changeset 
    28
 
  FinFun
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents: 63762
diff changeset 
    29
 
  Finite_Map
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28668
diff changeset 
    30
 
  Float
29688
6ed9ac8410d8 Added Formal_Power_Series in imports
chaieb
parents: 29650
diff changeset 
    31
 
  Formal_Power_Series
31761
3585bebe49a8 Added Library/Fraction_Field.thy: The fraction field of any integral
chaieb
parents: 31379
diff changeset 
    32
 
  Fraction_Field
53953
2f103a894ebe new theory of finite sets as a subtype
kuncar
parents: 52192
diff changeset 
    33
 
  FSet
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset 
    34
 
  FuncSet
48188
dcfe2c92fc7c Stub theory for division on functionals.
haftmann
parents: 48028
diff changeset 
    35
 
  Function_Division
51263
31e786e0e6a7 turned example into library for comparing growth of functions
haftmann
parents: 51174
diff changeset 
    36
 
  Function_Growth
29879
4425849f5db7 Moved FTA into Lib and cleaned it up a little.
nipkow
parents: 29847
diff changeset 
    37
 
  Fundamental_Theorem_Algebra
58196
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents: 58110
diff changeset 
    38
 
  Fun_Lexorder
58197
4fd7f47ead6c theory about sum and product on function bodies
haftmann
parents: 58196
diff changeset 
    39
 
  Groups_Big_Fun
37665
579258a77fec Add theory for indicator function.
hoelzl
parents: 37023
diff changeset 
    40
 
  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 
    41
 
  Infinite_Set
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents: 29987
diff changeset 
    42
 
  Inner_Product
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset 
    43
 
  IArray
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 34020
diff changeset 
    44
 
  Lattice_Algebras
30326
a01b2de0e3e1 constructive version of Cantor's first diagonalization argument
haftmann
parents: 30261
diff changeset 
    45
 
  Lattice_Syntax
57998
8b7508f848ef rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents: 57250
diff changeset 
    46
 
  Lattice_Constructions
58627
1329679abb2d add Linear Temporal Logic on Streams
hoelzl
parents: 58626
diff changeset 
    47
 
  Linear_Temporal_Logic_on_Streams
26173
5cac519abe4e renamed ListSpace to ListVector;
wenzelm
parents: 26170
diff changeset 
    48
 
  ListVector
58810
922a233805d2 more standard theory name;
wenzelm
parents: 58627
diff changeset 
    49
 
  Lub_Glb
29708
e40b70d38909 added Mapping.thy to Library
haftmann
parents: 29688
diff changeset 
    50
 
  Mapping
37790
7fea92005066 uniform do notation for monads
krauss
parents: 37789
diff changeset 
    51
 
  Monad_Syntax
58199
5fbe474b5da8 explicit theory with additional, less commonly used list operations
haftmann
parents: 58197
diff changeset 
    52
 
  More_List
59813
6320064f22bb more multiset theorems
blanchet
parents: 58810
diff changeset 
    53
 
  Multiset_Order
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24281
diff changeset 
    54
 
  Numeral_Type
61178
0b071f72f330 Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents: 60727
diff changeset 
    55
 
  Omega_Words_Fun
15470
7e12ad2f6672 added OptionalSugar
nipkow
parents: 15324
diff changeset 
    56
 
  OptionalSugar
26232
075264a0a4bc canonical order on option type
haftmann
parents: 26192
diff changeset 
    57
 
  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 
    58
 
  Order_Continuity
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset 
    59
 
  Parallel
63375
59803048b0e8 basic facts about almost everywhere fix bijections
haftmann
parents: 63317
diff changeset 
    60
 
  Perm
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset 
    61
 
  Permutation
44227
78e033e8ba05 get Library/Permutations.thy compiled and working again
huffman
parents: 44014
diff changeset 
    62
 
  Permutations
29987
391dcbd7e4dd move Polynomial.thy to Library
huffman
parents: 29986
diff changeset 
    63
 
  Polynomial
63317
ca187a9f66da Various additions to polynomials, FPSs, Gamma function
eberlm
parents: 63122
diff changeset 
    64
 
  Polynomial_FPS
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents: 30326
diff changeset 
    65
 
  Preorder
30019
a2f19e0a28b2 add theory of products as real vector spaces to Library
huffman
parents: 30018
diff changeset 
    66
 
  Product_Vector
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60141
diff changeset 
    67
 
  Quadratic_Discriminant
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    68
 
  Quotient_List
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    69
 
  Quotient_Option
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    70
 
  Quotient_Product
45074
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 44897
diff changeset 
    71
 
  Quotient_Set
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    72
 
  Quotient_Sum
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    73
 
  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 
    74
 
  Quotient_Type
21635
32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents: 21256
diff changeset 
    75
 
  Ramsey
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 29504
diff changeset 
    76
 
  Reflection
44818
27ba81ad0890 theory of saturated naturals contributed by Peter Gammie
haftmann
parents: 44561
diff changeset 
    77
 
  Saturated
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 37818
diff changeset 
    78
 
  Set_Algebras
63122
dd651e3f7413 Added set permutations/random permutations
eberlm
parents: 63071
diff changeset 
    79
 
  Set_Permutations
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset 
    80
 
  State_Monad
63071
3ca3bc795908 move Stirling numbers from AFP/Discrete_Summation
hoelzl
parents: 62692
diff changeset 
    81
 
  Stirling
58607
1f90ea1b4010 move Stream theory from Datatype_Examples to Library
hoelzl
parents: 58199
diff changeset 
    82
 
  Stream
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset 
    83
 
  Sublist
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 40673
diff changeset 
    84
 
  Sum_of_Squares
33649
854173fcd21c added a tabled implementation of the reflexive transitive closure
bulwahn
parents: 33356
diff changeset 
    85
 
  Transitive_Closure_Table
59928
b9b7f913a19a new theory Library/Tree_Multiset.thy
nipkow
parents: 59813
diff changeset 
    86
 
  Tree_Multiset
63762
6920b1885eff clarified session;
wenzelm
parents: 63464
diff changeset 
    87
 
  Type_Length
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset 
    88
 
  While_Combinator
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset 
    89
 
begin
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset 
    90
 
end
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset 
    91
 
(*>*)
isabelle