Moved Landau_Symbols from the AFP to HOL-Library

--HG--
extra : rebase_source : 118ac657be82d7b9b2d3e14ff4e59f8b1c3b7b5c

move FuncSet back to HOL-Library (amending 493b818e8e10)

--HG--
rename : src/HOL/FuncSet.thy => src/HOL/Library/FuncSet.thy

new tool Code_Lazy

added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly

--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy

clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
tuned headers;

--HG--
rename : src/Tools/Adhoc_Overloading.thy => src/HOL/Library/Adhoc_Overloading.thy
rename : src/Tools/adhoc_overloading.ML => src/HOL/Library/adhoc_overloading.ML

a conditional paramitrecity prover

removed mere toy example from library

--HG--
rename : src/HOL/Library/Function_Growth.thy => src/HOL/ex/Function_Growth.thy
extra : rebase_source : 3bb03a04a209b0755417d626db4b68d8265c0a44

add type of unordered pairs

reorganization of tree lemmas; new lemmas

HOL-Library: going_to filter

syntax for pattern aliases

--HG--
extra : amend_source : 7c0bbf9de4960ef668fef05070e84581f7ec7582

state monad

State_Monad ~> Open_State_Syntax

--HG--
rename : src/HOL/Library/State_Monad.thy => src/HOL/Library/Open_State_Syntax.thy

specific output setup is not supposed to intrude regular import theory

--HG--
extra : rebase_source : 51b89d836f6e8c4eddd8a3d48e85351a540784ab

session containing computational algebra

--HG--
rename : src/HOL/Number_Theory/Euclidean_Algorithm.thy => src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
rename : src/HOL/Number_Theory/Factorial_Ring.thy => src/HOL/Computational_Algebra/Factorial_Ring.thy
rename : src/HOL/Library/Formal_Power_Series.thy => src/HOL/Computational_Algebra/Formal_Power_Series.thy
rename : src/HOL/Library/Fundamental_Theorem_Algebra.thy => src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
rename : src/HOL/Library/Normalized_Fraction.thy => src/HOL/Computational_Algebra/Normalized_Fraction.thy
rename : src/HOL/Library/Polynomial.thy => src/HOL/Computational_Algebra/Polynomial.thy
rename : src/HOL/Library/Polynomial_FPS.thy => src/HOL/Computational_Algebra/Polynomial_FPS.thy
rename : src/HOL/Library/Polynomial_Factorial.thy => src/HOL/Computational_Algebra/Polynomial_Factorial.thy
rename : src/HOL/Number_Theory/Primes.thy => src/HOL/Computational_Algebra/Primes.thy
extra : rebase_source : c81da44950fdb70d0f6e552e1f73b980cac0ac75

re-established AFP entry for FinFuns as library

clarified library contents

--HG--
extra : rebase_source : 914de2d1cc30a640fae1e5a97b67b07637438a99

Library: fix name Product_plus to Product_Plus

--HG--
rename : src/HOL/Library/Product_plus.thy => src/HOL/Library/Product_Plus.thy

HOL-Analysis: move Product_Vector and Inner_Product from Library

--HG--
rename : src/HOL/Library/Inner_Product.thy => src/HOL/Analysis/Inner_Product.thy
rename : src/HOL/Library/Product_Vector.thy => src/HOL/Analysis/Product_Vector.thy

HOL-Analysis: move Continuum_Not_Denumerable from Library

--HG--
rename : src/HOL/Library/Continuum_Not_Denumerable.thy => src/HOL/Analysis/Continuum_Not_Denumerable.thy

HOL-Analysis: move Library/Convex to Convex_Euclidean_Space

--HG--
extra : rebase_source : 970dbe345b309706e87762ee13cc907b167f684b

Set_Permutations replaced by more general Multiset_Permutations

--HG--
extra : amend_source : 2cdc987e6383d982048c755e22fc87fcdc0e35cf

new type for finite maps; use it in HOL-Probability

clarified session;
misc tuning and modernization;

--HG--
rename : src/HOL/Word/Type_Length.thy => src/HOL/Library/Type_Length.thy

more standard name;

--HG--
rename : src/HOL/Library/ContNotDenum.thy => src/HOL/Library/Continuum_Not_Denumerable.thy

combinator to build partial equivalence relations from a predicate and an equivalenc relation

basic facts about almost everywhere fix bijections

Various additions to polynomials, FPSs, Gamma function

Added set permutations/random permutations

move Stirling numbers from AFP/Discrete_Summation

moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle

move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library

add extended nonnegative real numbers

--HG--
extra : rebase_source : ce03ad17148ce26b7b0e042b01890f086feeb79e

add countable complete lattices

--HG--
extra : rebase_source : 8433b3edbb76f8bfffd4954424a4990e24d82cf3

separated potentially conflicting type class instance into separate theory

add formalisation of Bourbaki-Witt fixpoint theorem

Omega_Words_Fun: Infinite words as functions from nat.

move disjoint sets to their own theory

--HG--
extra : rebase_source : f7ac738b5f7bae1fbeb64f65d618d9633cc24f25
extra : amend_source : cc60f0259364d5e70b189eb5321a49c655d6565d

tidying some messy proofs

New material, mostly about limits. Consolidation.

new theory Library/Tree_Multiset.thy

more multiset theorems

more standard theory name;

--HG--
rename : src/HOL/Library/Lubs_Glbs.thy => src/HOL/Library/Lub_Glb.thy

add Linear Temporal Logic on Streams

--HG--
extra : rebase_source : d68c2436a14ea4123ce9b4a90cef4caa7626b2fe
extra : amend_source : 1e25af333f240d1254bd3f073cc60ec95fb278d0

move Code_Test to HOL/Library;
add corresponding entries in NEWS and CONTRIBUTORS

--HG--
rename : src/HOL/Codegenerator_Test/Code_Test.thy => src/HOL/Library/Code_Test.thy
rename : src/HOL/Codegenerator_Test/code_test.ML => src/HOL/Library/code_test.ML

move Stream theory from Datatype_Examples to Library

--HG--
rename : src/HOL/Datatype_Examples/Stream.thy => src/HOL/Library/Stream.thy
extra : amend_source : e73f82c1bd2e07cabeaa7ac3f08f44cad2f2cec6

explicit theory with additional, less commonly used list operations

theory about sum and product on function bodies

theory about lexicographic ordering on functions

took out legacy material from 'HOL/Library/Library.thy'

renaming theory 'Old_SMT'

--HG--
rename : src/HOL/Library/SMT.thy => src/HOL/Library/Old_SMT.thy
rename : src/HOL/Library/SMT/smt_builtin.ML => src/HOL/Library/Old_SMT/smt_builtin.ML
rename : src/HOL/Library/SMT/smt_config.ML => src/HOL/Library/Old_SMT/smt_config.ML
rename : src/HOL/Library/SMT/smt_datatypes.ML => src/HOL/Library/Old_SMT/smt_datatypes.ML
rename : src/HOL/Library/SMT/smt_failure.ML => src/HOL/Library/Old_SMT/smt_failure.ML
rename : src/HOL/Library/SMT/smt_normalize.ML => src/HOL/Library/Old_SMT/smt_normalize.ML
rename : src/HOL/Library/SMT/smt_real.ML => src/HOL/Library/Old_SMT/smt_real.ML
rename : src/HOL/Library/SMT/smt_setup_solvers.ML => src/HOL/Library/Old_SMT/smt_setup_solvers.ML
rename : src/HOL/Library/SMT/smt_solver.ML => src/HOL/Library/Old_SMT/smt_solver.ML
rename : src/HOL/Library/SMT/smt_translate.ML => src/HOL/Library/Old_SMT/smt_translate.ML
rename : src/HOL/Library/SMT/smt_utils.ML => src/HOL/Library/Old_SMT/smt_utils.ML
rename : src/HOL/Library/SMT/smt_word.ML => src/HOL/Library/Old_SMT/smt_word.ML
rename : src/HOL/Library/SMT/smtlib_interface.ML => src/HOL/Library/Old_SMT/smtlib_interface.ML
rename : src/HOL/Library/SMT/z3_interface.ML => src/HOL/Library/Old_SMT/z3_interface.ML
rename : src/HOL/Library/SMT/z3_model.ML => src/HOL/Library/Old_SMT/z3_model.ML
rename : src/HOL/Library/SMT/z3_proof_literals.ML => src/HOL/Library/Old_SMT/z3_proof_literals.ML
rename : src/HOL/Library/SMT/z3_proof_methods.ML => src/HOL/Library/Old_SMT/z3_proof_methods.ML
rename : src/HOL/Library/SMT/z3_proof_parser.ML => src/HOL/Library/Old_SMT/z3_proof_parser.ML
rename : src/HOL/Library/SMT/z3_proof_reconstruction.ML => src/HOL/Library/Old_SMT/z3_proof_reconstruction.ML
rename : src/HOL/Library/SMT/z3_proof_tools.ML => src/HOL/Library/Old_SMT/z3_proof_tools.ML

moved old 'smt' method out of 'Main'

--HG--
rename : src/HOL/SMT.thy => src/HOL/Library/SMT.thy
rename : src/HOL/Tools/SMT/smt_builtin.ML => src/HOL/Library/SMT/smt_builtin.ML
rename : src/HOL/Tools/SMT/smt_config.ML => src/HOL/Library/SMT/smt_config.ML
rename : src/HOL/Tools/SMT/smt_datatypes.ML => src/HOL/Library/SMT/smt_datatypes.ML
rename : src/HOL/Tools/SMT/smt_failure.ML => src/HOL/Library/SMT/smt_failure.ML
rename : src/HOL/Tools/SMT/smt_normalize.ML => src/HOL/Library/SMT/smt_normalize.ML
rename : src/HOL/Tools/SMT/smt_real.ML => src/HOL/Library/SMT/smt_real.ML
rename : src/HOL/Tools/SMT/smt_setup_solvers.ML => src/HOL/Library/SMT/smt_setup_solvers.ML
rename : src/HOL/Tools/SMT/smt_solver.ML => src/HOL/Library/SMT/smt_solver.ML
rename : src/HOL/Tools/SMT/smt_translate.ML => src/HOL/Library/SMT/smt_translate.ML
rename : src/HOL/Tools/SMT/smt_utils.ML => src/HOL/Library/SMT/smt_utils.ML
rename : src/HOL/Tools/SMT/smtlib_interface.ML => src/HOL/Library/SMT/smtlib_interface.ML
rename : src/HOL/Tools/SMT/z3_interface.ML => src/HOL/Library/SMT/z3_interface.ML
rename : src/HOL/Tools/SMT/z3_model.ML => src/HOL/Library/SMT/z3_model.ML
rename : src/HOL/Tools/SMT/z3_proof_literals.ML => src/HOL/Library/SMT/z3_proof_literals.ML
rename : src/HOL/Tools/SMT/z3_proof_methods.ML => src/HOL/Library/SMT/z3_proof_methods.ML
rename : src/HOL/Tools/SMT/z3_proof_parser.ML => src/HOL/Library/SMT/z3_proof_parser.ML
rename : src/HOL/Tools/SMT/z3_proof_reconstruction.ML => src/HOL/Library/SMT/z3_proof_reconstruction.ML
rename : src/HOL/Tools/SMT/z3_proof_tools.ML => src/HOL/Library/SMT/z3_proof_tools.ML

rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup

--HG--
rename : src/HOL/Library/Quickcheck_Types.thy => src/HOL/Library/Lattice_Constructions.thy

new theory of binary trees

removed Kleene_Algebra because of superior AFP entry; authors agreed

add various lemmas

bnf_decl -> bnf_axiomatization

--HG--
rename : src/HOL/Library/BNF_Decl.thy => src/HOL/Library/BNF_Axiomatization.thy

proper inclusion into library

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

--HG--
rename : src/HOL/Library/Continuity.thy => src/HOL/Library/Order_Continuity.thy
extra : rebase_source : d8ac7002419cf6199ad52baea5d24cbc0e1a47e7

Replacing the theory Library/Binomial by Number_Theory/Binomial

--HG--
rename : src/Doc/Tutorial/Rules/Primes.thy => src/Doc/Tutorial/Rules/TPrimes.thy

killed 'More_BNFs' by moving its various bits where they (now) belong

dissolved BNF session

--HG--
rename : src/HOL/BNF/BNF_Decl.thy => src/HOL/Library/BNF_Decl.thy
rename : src/HOL/Cardinals/Cardinal_Notations.thy => src/HOL/Library/Cardinal_Notations.thy
rename : src/HOL/BNF/Countable_Set_Type.thy => src/HOL/Library/Countable_Set_Type.thy
rename : src/HOL/BNF/More_BNFs.thy => src/HOL/Library/More_BNFs.thy
rename : src/HOL/BNF/Tools/bnf_decl.ML => src/HOL/Library/bnf_decl.ML

moved 'Zorn' into 'Main', since it's a BNF dependency

--HG--
rename : src/HOL/Library/Zorn.thy => src/HOL/Zorn.thy

adapted to move of Wfrec

Add Zorn to HOL-Library

effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies

--HG--
rename : src/HOL/Library/Order_Union.thy => src/HOL/Cardinals/Order_Union.thy

more convenient place for a theory in solitariness

--HG--
rename : src/HOL/Library/Abstract_Rat.thy => src/HOL/Decision_Procs/Rat_Pair.thy
extra : rebase_source : e6cf0e927b0785b5f336013cf54f27492203772b

consolidated clone theory

--HG--
extra : rebase_source : fc02fc4ce5406ef4ae16f255b5b0504553600111

new theory of finite sets as a subtype

actually test theory Order_Union;

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

tuned imports;

discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types

New theory of infinity-extended types; should replace Extended_xyz eventually

turned example into library for comparing growth of functions

--HG--
rename : src/HOL/ex/Landau.thy => src/HOL/Library/Function_Growth.thy

fundamentals about discrete logarithm and square root

attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary

--HG--
rename : src/HOL/Codegenerator_Test/Generate_Pretty.thy => src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
rename : src/HOL/Codegenerator_Test/RBT_Set_Test.thy => src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
rename : src/HOL/Codegenerator_Test/Generate_Pretty.thy => src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
rename : src/HOL/Codegenerator_Test/Generate_Pretty.thy => src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
extra : rebase_source : 23f4210ddd8c114024c8573417949dccb5e29ba6

add Countable_Set theory

regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards

--HG--
extra : rebase_source : f535a1f0a613567ad927269eca5c0ba4e00f737b

explicit FIXME;

implementation of sets by RBT trees for the code generator

library theories for debugging and parallel computing using code generation towards Isabelle/ML

explicitly import Dlist theory into library

Stub theory for division on functionals.

move FinFuns from AFP to repository

dropped now obsolete Cset theories

incorporated More_Set and More_List into the Main body -- to be consolidated later

--HG--
rename : src/HOL/Library/More_List.thy => src/HOL/More_List.thy
rename : src/HOL/Library/More_Set.thy => src/HOL/More_Set.thy

remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality

Quotient_Set.thy is part of library

moving connection of association lists to Mappings into a separate theory

--HG--
rename : src/HOL/Library/AssocList.thy => src/HOL/Library/AList_Impl.thy

theory of saturated naturals contributed by Peter Gammie

avoid loading List_Cset and Dlist_Cet at the same time

moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

--HG--
rename : src/HOL/Library/Nested_Environment.thy => src/HOL/Unix/Nested_Environment.thy

get Library/Permutations.thy compiled and working again

moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef

moved recdef package to HOL/Library/Old_Recdef.thy

--HG--
rename : src/HOL/Recdef.thy => src/HOL/Library/Old_Recdef.thy

Add theory for setting up monad syntax for Cset

removing SML_Quickcheck

rename Nat_Infinity (inat) to Extended_Nat (enat)

--HG--
rename : src/HOL/Library/Nat_Infinity.thy => src/HOL/Library/Extended_Nat.thy

splitting Cset into Cset and List_Cset

splitting Dlist theory in Dlist and Dlist_Cset

splitting RBT theory into RBT and RBT_Mapping

renamed Sum_Of_Squares to Sum_of_Squares;

--HG--
rename : src/HOL/Library/Sum_Of_Squares.thy => src/HOL/Library/Sum_of_Squares.thy
rename : src/HOL/Library/Sum_Of_Squares/etc/settings => src/HOL/Library/Sum_of_Squares/etc/settings
rename : src/HOL/Library/Sum_Of_Squares/neos_csdp_client => src/HOL/Library/Sum_of_Squares/neos_csdp_client
rename : src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML => src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
rename : src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML => src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
rename : src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML => src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

replaced misleading Fset/fset name -- these do not stand for finite sets

--HG--
rename : src/HOL/Library/Fset.thy => src/HOL/Library/Cset.thy

adding Enum to HOL-Main image and removing it from HOL-Library

moved theory Quicksort from Library/ to ex/

--HG--
rename : src/HOL/Library/Quicksort.thy => src/HOL/ex/Quicksort.thy

split and enriched theory SetsAndFunctions

--HG--
rename : src/HOL/Library/SetsAndFunctions.thy => src/HOL/Library/Function_Algebras.thy
rename : src/HOL/Library/SetsAndFunctions.thy => src/HOL/Library/Set_Algebras.thy

load cache_io before code generator; moved adhoc-overloading to generic tools

--HG--
rename : src/HOL/Library/Adhoc_Overloading.thy => src/Tools/Adhoc_Overloading.thy
rename : src/HOL/Library/adhoc_overloading.ML => src/Tools/adhoc_overloading.ML

uniform do notation for monads

generic ad-hoc overloading via check/uncheck

remove codegeneration-related theories from big library theory

Add theory for indicator function.

added theory More_List

dropped old Library/Word.thy and toy example ex/Adder.thy

Add Convex to Library build

theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

--HG--
rename : src/HOL/Library/Table.thy => src/HOL/Library/RBT.thy
rename : src/HOL/Library/RBT.thy => src/HOL/Library/RBT_Impl.thy

removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;

added Table.thy

added Dlist

Initial version of HOL quotient package.

renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;

--HG--
rename : src/HOL/Library/Quotient.thy => src/HOL/Library/Quotient_Type.thy

revert uninspired Structure_Syntax experiment

separate library theory for type classes combining lattices with various algebraic structures

separate theory for index structures

merged Crude_Executable_Set into Executable_Set

--HG--
rename : src/HOL/Library/Crude_Executable_Set.thy => src/HOL/Library/Executable_Set.thy

added Crude_Executable_Set.thy

added a tabled implementation of the reflexive transitive closure

moved Commutative_Ring into session Decision_Procs

--HG--
rename : src/HOL/Library/Commutative_Ring.thy => src/HOL/Decision_Procs/Commutative_Ring.thy
rename : src/HOL/ex/Commutative_Ring_Complete.thy => src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
rename : src/HOL/Library/comm_ring.ML => src/HOL/Decision_Procs/commutative_ring_tac.ML
rename : src/HOL/ex/Commutative_RingEx.thy => src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy

re-moved theory Fin_Fun to AFP

turned off old quickcheck

distinguished session for multivariate analysis

some reorganization of number theory

--HG--
rename : src/HOL/NewNumberTheory/Binomial.thy => src/HOL/Number_Theory/Binomial.thy
rename : src/HOL/NewNumberTheory/Cong.thy => src/HOL/Number_Theory/Cong.thy
rename : src/HOL/NewNumberTheory/Fib.thy => src/HOL/Number_Theory/Fib.thy
rename : src/HOL/NewNumberTheory/MiscAlgebra.thy => src/HOL/Number_Theory/MiscAlgebra.thy
rename : src/HOL/GCD.thy => src/HOL/Number_Theory/Primes.thy
rename : src/HOL/NewNumberTheory/ROOT.ML => src/HOL/Number_Theory/ROOT.ML
rename : src/HOL/NewNumberTheory/Residues.thy => src/HOL/Number_Theory/Residues.thy
rename : src/HOL/NewNumberTheory/UniqueFactorization.thy => src/HOL/Number_Theory/UniqueFactorization.thy
rename : src/HOL/NumberTheory/BijectionRel.thy => src/HOL/Old_Number_Theory/BijectionRel.thy
rename : src/HOL/NumberTheory/Chinese.thy => src/HOL/Old_Number_Theory/Chinese.thy
rename : src/HOL/NumberTheory/Euler.thy => src/HOL/Old_Number_Theory/Euler.thy
rename : src/HOL/NumberTheory/EulerFermat.thy => src/HOL/Old_Number_Theory/EulerFermat.thy
rename : src/HOL/NumberTheory/EvenOdd.thy => src/HOL/Old_Number_Theory/EvenOdd.thy
rename : src/HOL/NumberTheory/Factorization.thy => src/HOL/Old_Number_Theory/Factorization.thy
rename : src/HOL/NumberTheory/Fib.thy => src/HOL/Old_Number_Theory/Fib.thy
rename : src/HOL/NumberTheory/Finite2.thy => src/HOL/Old_Number_Theory/Finite2.thy
rename : src/HOL/NumberTheory/Gauss.thy => src/HOL/Old_Number_Theory/Gauss.thy
rename : src/HOL/NumberTheory/Int2.thy => src/HOL/Old_Number_Theory/Int2.thy
rename : src/HOL/NumberTheory/IntFact.thy => src/HOL/Old_Number_Theory/IntFact.thy
rename : src/HOL/NumberTheory/IntPrimes.thy => src/HOL/Old_Number_Theory/IntPrimes.thy
rename : src/HOL/Library/Legacy_GCD.thy => src/HOL/Old_Number_Theory/Legacy_GCD.thy
rename : src/HOL/Library/Pocklington.thy => src/HOL/Old_Number_Theory/Pocklington.thy
rename : src/HOL/Library/Primes.thy => src/HOL/Old_Number_Theory/Primes.thy
rename : src/HOL/NumberTheory/Quadratic_Reciprocity.thy => src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
rename : src/HOL/NumberTheory/ROOT.ML => src/HOL/Old_Number_Theory/ROOT.ML
rename : src/HOL/NumberTheory/Residues.thy => src/HOL/Old_Number_Theory/Residues.thy
rename : src/HOL/NumberTheory/WilsonBij.thy => src/HOL/Old_Number_Theory/WilsonBij.thy
rename : src/HOL/NumberTheory/WilsonRuss.thy => src/HOL/Old_Number_Theory/WilsonRuss.thy
rename : src/HOL/NumberTheory/document/root.tex => src/HOL/Old_Number_Theory/document/root.tex

move Kleene_Algebra to Library

renamed theory Code_Set to Fset

--HG--
rename : src/HOL/Library/Code_Set.thy => src/HOL/Library/Fset.thy

Added Library/Fraction_Field.thy: The fraction field of any integral
domain

added List_Set and Code_Set theories

added Fin_Fun theory

Added Convex_Euclidean_Space.thy again.

Removed Convex_Euclidean_Space.thy from Library.

Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile

experimental move of Quickcheck and related theories to HOL image

--HG--
rename : src/HOL/Library/Code_Index.thy => src/HOL/Code_Index.thy
rename : src/HOL/Library/Quickcheck.thy => src/HOL/Quickcheck.thy
rename : src/HOL/Library/Random.thy => src/HOL/Random.thy

Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library

added theory for explicit equivalence relation in preorders

constructive version of Cantor's first diagonalization argument

Added Libray dependency on Topology_Euclidean_Space

Merge.

add theory of products as real vector spaces to Library

add new theory Product_plus.thy to Library

add formalization of a type of integers mod 2 to Library

new theory of real inner product spaces

move Polynomial.thy to Library

--HG--
rename : src/HOL/Polynomial.thy => src/HOL/Library/Polynomial.thy

move FrechetDeriv.thy to Library

--HG--
rename : src/HOL/FrechetDeriv.thy => src/HOL/Library/FrechetDeriv.thy

split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy

Moved FTA into Lib and cleaned it up a little.

--HG--
rename : src/HOL/Fundamental_Theorem_Algebra.thy => src/HOL/Library/Fundamental_Theorem_Algebra.thy

Added HOL/Library/Finite_Cartesian_Product.thy to Library

added Determinants to Library

added Euclidean_Space and Glbs to Library

session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there

--HG--
rename : src/HOL/Reflection/Approximation.thy => src/HOL/Decision_Procs/Approximation.thy
rename : src/HOL/Reflection/Cooper.thy => src/HOL/Decision_Procs/Cooper.thy
rename : src/HOL/Library/Dense_Linear_Order.thy => src/HOL/Decision_Procs/Dense_Linear_Order.thy
rename : src/HOL/Reflection/Ferrack.thy => src/HOL/Decision_Procs/Ferrack.thy
rename : src/HOL/Reflection/MIR.thy => src/HOL/Decision_Procs/MIR.thy
rename : src/HOL/Reflection/ROOT.ML => src/HOL/Decision_Procs/ROOT.ML
rename : src/HOL/Reflection/cooper_tac.ML => src/HOL/Decision_Procs/cooper_tac.ML
rename : src/HOL/Reflection/ferrack_tac.ML => src/HOL/Decision_Procs/ferrack_tac.ML
rename : src/HOL/Reflection/mir_tac.ML => src/HOL/Decision_Procs/mir_tac.ML

fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library

moved Random.thy to Library

--HG--
rename : src/HOL/ex/Random.thy => src/HOL/Library/Random.thy

added Mapping.thy to Library

Added Formal_Power_Series in imports

Reflection.thy now in HOL/Library

--HG--
rename : src/HOL/ex/Reflection.thy => src/HOL/Library/Reflection.thy
rename : src/HOL/ex/reflection.ML => src/HOL/Library/reflection.ML
rename : src/HOL/ex/reflection_data.ML => src/HOL/Library/reify_data.ML

moved Univ_Poly to Library

--HG--
rename : src/HOL/Univ_Poly.thy => src/HOL/Library/Univ_Poly.thy

split of Imperative_HOL theories from HOL-Library

--HG--
rename : src/HOL/Library/Array.thy => src/HOL/Imperative_HOL/Array.thy
rename : src/HOL/Library/Heap.thy => src/HOL/Imperative_HOL/Heap.thy
rename : src/HOL/Library/Heap_Monad.thy => src/HOL/Imperative_HOL/Heap_Monad.thy
rename : src/HOL/Library/Imperative_HOL.thy => src/HOL/Imperative_HOL/Imperative_HOL.thy
rename : src/HOL/Library/Ref.thy => src/HOL/Imperative_HOL/Ref.thy
rename : src/HOL/Library/Relational.thy => src/HOL/Imperative_HOL/Relational.thy
rename : src/HOL/Library/Subarray.thy => src/HOL/ex/Subarray.thy
rename : src/HOL/Library/Sublist.thy => src/HOL/ex/Sublist.thy

adapted HOL source structure to distribution layout

--HG--
rename : src/HOL/Library/Dense_Linear_Order.thy => src/HOL/Dense_Linear_Order.thy
rename : src/HOL/Complex/Fundamental_Theorem_Algebra.thy => src/HOL/Fundamental_Theorem_Algebra.thy
rename : src/HOL/Real/HahnBanach/Bounds.thy => src/HOL/HahnBanach/Bounds.thy
rename : src/HOL/Real/HahnBanach/FunctionNorm.thy => src/HOL/HahnBanach/FunctionNorm.thy
rename : src/HOL/Real/HahnBanach/FunctionOrder.thy => src/HOL/HahnBanach/FunctionOrder.thy
rename : src/HOL/Real/HahnBanach/HahnBanach.thy => src/HOL/HahnBanach/HahnBanach.thy
rename : src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy => src/HOL/HahnBanach/HahnBanachExtLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachLemmas.thy => src/HOL/HahnBanach/HahnBanachLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy => src/HOL/HahnBanach/HahnBanachSupLemmas.thy
rename : src/HOL/Real/HahnBanach/Linearform.thy => src/HOL/HahnBanach/Linearform.thy
rename : src/HOL/Real/HahnBanach/NormedSpace.thy => src/HOL/HahnBanach/NormedSpace.thy
rename : src/HOL/Real/HahnBanach/README.html => src/HOL/HahnBanach/README.html
rename : src/HOL/Real/HahnBanach/ROOT.ML => src/HOL/HahnBanach/ROOT.ML
rename : src/HOL/Real/HahnBanach/Subspace.thy => src/HOL/HahnBanach/Subspace.thy
rename : src/HOL/Real/HahnBanach/VectorSpace.thy => src/HOL/HahnBanach/VectorSpace.thy
rename : src/HOL/Real/HahnBanach/ZornLemma.thy => src/HOL/HahnBanach/ZornLemma.thy
rename : src/HOL/Real/HahnBanach/document/root.bib => src/HOL/HahnBanach/document/root.bib
rename : src/HOL/Real/HahnBanach/document/root.tex => src/HOL/HahnBanach/document/root.tex
rename : src/HOL/Real/RealVector.thy => src/HOL/RealVector.thy
rename : src/HOL/Hyperreal/SEQ.thy => src/HOL/SEQ.thy

moved ContNotDenum into Library

--HG--
rename : src/HOL/ContNotDenum.thy => src/HOL/Library/ContNotDenum.thy

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML

fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;

evaluation using code generator

Replaced Library/NatPair by Nat_Int_Bij.

refined code generator setup for rational numbers; more simplification rules for rational numbers

add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)

established Plain theory and image

moved Float.thy to Library

added theory Library/Enum.thy

Added Order_Relation

canonical order on option type

new theory of red-black trees, an efficient implementation of finite maps.

renamed ListSpace to ListVector;

added theories for imperative HOL

Loads Dense_Linear_Order.thy

Uses Univ_Poly.thy

*** empty log message ***

removed dependencies on Size_Change_Termination from HOL-Library;

consolidated naming conventions for code generator theories

introduced generic concepts for theory interpretators

Added function package to PreList
Added sorted/sort to List
Moved qsort from ex to Library

Integrated Executable_Rat and Executable_Real theories into
Rational and RealDef theories.

boolean algebras as locales and numbers as types by Brian Huffman

added Eval_Witness theory

proper implementation of rational numbers

uniform naming conventions for CG theories

Moved list comprehension into List

Added List_Comprehension

A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;

moved code generation pretty integers and characters to separate theories

importing Eval theory

Added formalization of size-change principle (experimental).

added Ramsey.thy to Library imports, to include it in the daily builds

moved theories Parity, GCD, Binomial to Library;

added state monad to HOL library

moved theory Infinite_Set to Library;

added some codegen examples/applications

added ExecutableRat.thy

First usable version of the new function definition package (HOL/function_packake/...).
Moved Accessible_Part.thy from Library to Main.

moved arithmetic series to geometric series in SetInterval

renamed ASeries to Arithmetic_Series, removed the ^M

Added Library/AssocList.thy

* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)

added HOL/Library/Coinductive_List.thy;

Added ExecutableSet.

added Commutative_Ring (from Main HOL);

1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML

Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy

Removes an inconsistent definition from Library.thy ,
so that the lexical order is the standard order for lists.
The prefix order is not built any more.

Removed dir Orderings in Library

added OptionalSugar

Added EfficientNat

import -> imports

New theory header syntax.

tuned document;

Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
to HOL/ex.

replacing HOL/Real/PRat, PNat by the rational number development
of Markus Wenzel

conversion of integers to use Ring_and_Field;
new lemmas for Ring_and_Field

new theory NatPair of the injection from nat*nat -> nat

tuned Primes theory;

added Library/Nat_Infinity.thy and Library/Continuity.thy

added Permutation;

Merged Example into While_Combi

Ring_and_Field_Example;

added HOL/Library/Nested_Environment.thy;

activate Rational_Numbers;

deactivate Rational_Numbers (tmp!);

Rational_Numbers;

Ring_and_Field;

added List_Prefix;

"The Supplemental Isabelle/HOL Library";