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 desharna
Tue, 11 Jun 2024 10:27:35 +0200
changeset 80345 7d4cd57cd955
parent 79936 eb753708e85b
child 81467 3fab5b28027d
permissions -rw-r--r--
tuned proof
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73034
43c534bba442 tuned whitespace (amending a4bffc0de967);
wenzelm
parents: 72515
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
68061
81d90f830f99 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
wenzelm
parents: 67224
diff changeset 
     5
 
  Adhoc_Overloading
56942
5fff4dc31d34 bnf_decl -> bnf_axiomatization
traytel
parents: 56415
diff changeset 
     6
 
  BNF_Axiomatization
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents: 62652
diff changeset 
     7
 
  BNF_Corec
61766
507b39df1a57 add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents: 61178
diff changeset 
     8
 
  Bourbaki_Witt_Fixpoint
77884
0e054e6e7f5e clarified terminology
haftmann
parents: 77003
diff changeset 
     9
 
  Centered_Division
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21192
diff changeset 
    10
 
  Char_ord
73886
93ba8e3fdcdf move code setup from Cardinality to separate theory
Andreas Lochbihler <mail@andreas-lochbihler.de>
parents: 73622
diff changeset 
    11
 
  Code_Cardinality
68155
8b50f29a1992 new tool Code_Lazy
Andreas Lochbihler
parents: 68073
diff changeset 
    12
 
  Code_Lazy
58626
6c473ed0ac70 move Code_Test to HOL/Library;
Andreas Lochbihler
parents: 58607
diff changeset 
    13
 
  Code_Test
63377
64adf4ba9526 combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents: 63375
diff changeset 
    14
 
  Combine_PER
62652
7248d106c607 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents: 62375
diff changeset 
    15
 
  Complete_Partial_Order2
67224
341fbce5b26d a conditional paramitrecity prover
traytel
parents: 66797
diff changeset 
    16
 
  Conditional_Parametricity
71393
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71036
diff changeset 
    17
 
  Confluence
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71036
diff changeset 
    18
 
  Confluent_Quotient
26170
66e6b967ccf1 added theories for imperative HOL
haftmann
parents: 26157
diff changeset 
    19
 
  Countable
62373
ea7a442e9a56 add countable complete lattices
hoelzl
parents: 62352
diff changeset 
    20
 
  Countable_Complete_Lattices
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55018
diff changeset 
    21
 
  Countable_Set_Type
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset 
    22
 
  Debug
50087
635d73673b5e regularity of measures, therefore:
immler
parents: 48742
diff changeset 
    23
 
  Diagonal_Subsequence
66797
9c9baae29217 removed mere toy example from library
haftmann
parents: 66563
diff changeset 
    24
 
  Discrete
60727
53697011b03a move disjoint sets to their own theory
hoelzl
parents: 60162
diff changeset 
    25
 
  Disjoint_Sets
73326
7a88313895d5 dissolve theory with duplicated name from afp
haftmann
parents: 73297
diff changeset 
    26
 
  Disjoint_FSets
48283
8a1ef12f7e6d explicitly import Dlist theory into library
haftmann
parents: 48188
diff changeset 
    27
 
  Dlist
69909
5382f5691a11 proper theory for type of dual ordered lattice in distribution
haftmann
parents: 69790
diff changeset 
    28
 
  Dual_Ordered_Lattice
69735
8230dca028eb the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents: 69194
diff changeset 
    29
 
  Equipollence
51542
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    30
 
  Extended
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    31
 
  Extended_Nat
62375
670063003ad3 add extended nonnegative real numbers
hoelzl
parents: 62373
diff changeset 
    32
 
  Extended_Nonnegative_Real
51542
738598beeb26 tuned imports;
wenzelm
parents: 51382
diff changeset 
    33
 
  Extended_Real
63885
a6cd18af8bf9 new type for finite maps; use it in HOL-Probability
Lars Hupel <lars.hupel@mytum.de>
parents: 63762
diff changeset 
    34
 
  Finite_Map
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28668
diff changeset 
    35
 
  Float
53953
2f103a894ebe new theory of finite sets as a subtype
kuncar
parents: 52192
diff changeset 
    36
 
  FSet
68188
2af1f142f855 move FuncSet back to HOL-Library (amending 493b818e8e10)
immler
parents: 68155
diff changeset 
    37
 
  FuncSet
48188
dcfe2c92fc7c Stub theory for division on functionals.
haftmann
parents: 48028
diff changeset 
    38
 
  Function_Division
58196
1b3fbfb85980 theory about lexicographic ordering on functions
haftmann
parents: 58110
diff changeset 
    39
 
  Fun_Lexorder
66488
9d83e8fe3de3 HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents: 66451
diff changeset 
    40
 
  Going_To_Filter
58197
4fd7f47ead6c theory about sum and product on function bodies
haftmann
parents: 58196
diff changeset 
    41
 
  Groups_Big_Fun
37665
579258a77fec Add theory for indicator function.
hoelzl
parents: 37023
diff changeset 
    42
 
  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 
    43
 
  Infinite_Set
79597
76a1c0ea6777 A few lemmas brought in from AFP entries
paulson <lp15@cam.ac.uk>
parents: 77884
diff changeset 
    44
 
  Infinite_Typeclass
71035
6fe5a0e1fa8e moved theory Interval from the AFP
immler
parents: 70342
diff changeset 
    45
 
  Interval
71036
dfcc1882d05a moved theory Interval_Approximation from the AFP
immler
parents: 71035
diff changeset 
    46
 
  Interval_Float
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset 
    47
 
  IArray
68246
b48bab511939 Moved Landau_Symbols from the AFP to HOL-Library
Manuel Eberl <eberlm@in.tum.de>
parents: 68188
diff changeset 
    48
 
  Landau_Symbols
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 34020
diff changeset 
    49
 
  Lattice_Algebras
57998
8b7508f848ef rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents: 57250
diff changeset 
    50
 
  Lattice_Constructions
58627
1329679abb2d add Linear Temporal Logic on Streams
hoelzl
parents: 58626
diff changeset 
    51
 
  Linear_Temporal_Logic_on_Streams
26173
5cac519abe4e renamed ListSpace to ListVector;
wenzelm
parents: 26170
diff changeset 
    52
 
  ListVector
58810
922a233805d2 more standard theory name;
wenzelm
parents: 58627
diff changeset 
    53
 
  Lub_Glb
29708
e40b70d38909 added Mapping.thy to Library
haftmann
parents: 29688
diff changeset 
    54
 
  Mapping
37790
7fea92005066 uniform do notation for monads
krauss
parents: 37789
diff changeset 
    55
 
  Monad_Syntax
58199
5fbe474b5da8 explicit theory with additional, less commonly used list operations
haftmann
parents: 58197
diff changeset 
    56
 
  More_List
59813
6320064f22bb more multiset theorems
blanchet
parents: 58810
diff changeset 
    57
 
  Multiset_Order
75801
5c1856aaf03d New theory of fixed length lists
nipkow
parents: 74334
diff changeset 
    58
 
  NList
64588
293ab573d034 clarified library contents
haftmann
parents: 63972
diff changeset 
    59
 
  Nonpos_Ints
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24281
diff changeset 
    60
 
  Numeral_Type
61178
0b071f72f330 Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents: 60727
diff changeset 
    61
 
  Omega_Words_Fun
66270
403d84138c5c State_Monad ~> Open_State_Syntax
Lars Hupel <lars.hupel@mytum.de>
parents: 66015
diff changeset 
    62
 
  Open_State_Syntax
26232
075264a0a4bc canonical order on option type
haftmann
parents: 26192
diff changeset 
    63
 
  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 
    64
 
  Order_Continuity
48427
571cb1df0768 library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents: 48283
diff changeset 
    65
 
  Parallel
66451
5be0b0604d71 syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset 
    66
 
  Pattern_Aliases
64588
293ab573d034 clarified library contents
haftmann
parents: 63972
diff changeset 
    67
 
  Periodic_Fun
70042
45787384ff86 new theory Library/Poly_Mapping, of almost-everywhere-zero functions
paulson <lp15@cam.ac.uk>
parents: 69909
diff changeset 
    68
 
  Poly_Mapping
69790
154cf64e403e Exponentiation by squaring, fast modular exponentiation
Manuel Eberl <eberlm@in.tum.de>
parents: 69735
diff changeset 
    69
 
  Power_By_Squaring
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents: 30326
diff changeset 
    70
 
  Preorder
63972
c98d1dd7eba1 Library: fix name Product_plus to Product_Plus
hoelzl
parents: 63971
diff changeset 
    71
 
  Product_Plus
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60141
diff changeset 
    72
 
  Quadratic_Discriminant
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    73
 
  Quotient_List
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    74
 
  Quotient_Option
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    75
 
  Quotient_Product
45074
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 44897
diff changeset 
    76
 
  Quotient_Set
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    77
 
  Quotient_Sum
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35100
diff changeset 
    78
 
  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 
    79
 
  Quotient_Type
21635
32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents: 21256
diff changeset 
    80
 
  Ramsey
79936
eb753708e85b HOL-Library: added modulo/congruence for real numbers
Manuel Eberl <eberlm@in.tum.de>
parents: 79597
diff changeset 
    81
 
  Real_Mod
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 29504
diff changeset 
    82
 
  Reflection
64588
293ab573d034 clarified library contents
haftmann
parents: 63972
diff changeset 
    83
 
  Rewrite
44818
27ba81ad0890 theory of saturated naturals contributed by Peter Gammie
haftmann
parents: 44561
diff changeset 
    84
 
  Saturated
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 37818
diff changeset 
    85
 
  Set_Algebras
69004
f6a0c8115e9c Set idioms theory "finite intersection_of open", etc.
paulson <lp15@cam.ac.uk>
parents: 68246
diff changeset 
    86
 
  Set_Idioms
72281
beeadb35e357 more thorough treatment of division, particularly signed division on int and word
haftmann
parents: 71956
diff changeset 
    87
 
  Signed_Division
66271
d157195a468a state monad
Lars Hupel <lars.hupel@mytum.de>
parents: 66270
diff changeset 
    88
 
  State_Monad
58607
1f90ea1b4010 move Stream theory from Datatype_Examples to Library
hoelzl
parents: 58199
diff changeset 
    89
 
  Stream
69194
6d514e128a85 dedicated theory for sorting algorithms
haftmann
parents: 69184
diff changeset 
    90
 
  Sorting_Algorithms
51161
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents: 50134
diff changeset 
    91
 
  Sublist
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 40673
diff changeset 
    92
 
  Sum_of_Squares
33649
854173fcd21c added a tabled implementation of the reflexive transitive closure
bulwahn
parents: 33356
diff changeset 
    93
 
  Transitive_Closure_Table
59928
b9b7f913a19a new theory Library/Tree_Multiset.thy
nipkow
parents: 59813
diff changeset 
    94
 
  Tree_Multiset
66510
ca7a369301f6 reorganization of tree lemmas; new lemmas
nipkow
parents: 66488
diff changeset 
    95
 
  Tree_Real
63762
6920b1885eff clarified session;
wenzelm
parents: 63464
diff changeset 
    96
 
  Type_Length
66563
87b9eb69d5ba add type of unordered pairs
Andreas Lochbihler
parents: 66510
diff changeset 
    97
 
  Uprod
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset 
    98
 
  While_Combinator
72515
c7038c397ae3 moved most material from session HOL-Word to Word_Lib in the AFP
haftmann
parents: 72281
diff changeset 
    99
 
  Word
70342
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 70042
diff changeset 
   100
 
  Z2
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14706
diff changeset 
   101
 
begin
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset 
   102
 
end
66451
5be0b0604d71 syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents: 66271
diff changeset 
   103
 
(*>*)
isabelle