23 months ago haftmann [Wed, 17 Feb 2016 21:51:57 +0100] rev 62347
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
NEWS src/HOL/Algebra/Coset.thy src/HOL/Binomial.thy src/HOL/Fields.thy src/HOL/GCD.thy src/HOL/Groups.thy src/HOL/Int.thy src/HOL/NthRoot.thy src/HOL/Power.thy src/HOL/Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Rings.thy src/HOL/Transcendental.thy

23 months ago haftmann [Wed, 17 Feb 2016 21:51:56 +0100] rev 62346
more theorems concerning gcd/lcm/Gcd/Lcm
src/HOL/GCD.thy

23 months ago haftmann [Wed, 17 Feb 2016 21:51:56 +0100] rev 62345
further generalization and polishing
NEWS src/HOL/GCD.thy

23 months ago haftmann [Wed, 17 Feb 2016 21:51:56 +0100] rev 62344
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
src/HOL/Binomial.thy src/HOL/GCD.thy src/HOL/Nat.thy

23 months ago haftmann [Wed, 17 Feb 2016 21:51:56 +0100] rev 62343
prefer abbreviations for compound operators INFIMUM and SUPREMUM
CONTRIBUTORS NEWS src/HOL/Algebra/AbelCoset.thy src/HOL/Algebra/Coset.thy src/HOL/Auth/Guard/Proto.thy src/HOL/Auth/Message.thy src/HOL/Auth/Recur.thy src/HOL/Auth/Smartcard/ShoupRubin.thy src/HOL/Auth/Smartcard/ShoupRubinBella.thy src/HOL/Auth/Smartcard/Smartcard.thy src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/Cardinals/Wellorder_Relation.thy src/HOL/Complete_Lattices.thy src/HOL/Conditionally_Complete_Lattices.thy src/HOL/Enum.thy src/HOL/Filter.thy src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy src/HOL/Hoare_Parallel/OG_Hoare.thy src/HOL/Hoare_Parallel/RG_Hoare.thy src/HOL/IMP/Denotational.thy src/HOL/Library/Countable_Set_Type.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/FSet.thy src/HOL/Library/Finite_Lattice.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Liminf_Limsup.thy src/HOL/Library/Lub_Glb.thy src/HOL/Library/Option_ord.thy src/HOL/Library/Product_Order.thy src/HOL/Lifting_Set.thy src/HOL/List.thy src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Number_Theory/MiscAlgebra.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Complete_Measure.thy src/HOL/Probability/Embed_Measure.thy src/HOL/Probability/Fin_Map.thy src/HOL/Probability/Independent_Family.thy src/HOL/Probability/Infinite_Product_Measure.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measurable.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy src/HOL/Probability/Probability_Measure.thy ...

23 months ago haftmann [Wed, 17 Feb 2016 21:51:55 +0100] rev 62342
consolidated name
src/HOL/Decision_Procs/Cooper.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/hologic.ML src/HOL/Tools/lin_arith.ML

23 months ago wenzelm [Wed, 17 Feb 2016 21:08:18 +0100] rev 62341
merged

23 months ago wenzelm [Wed, 17 Feb 2016 21:08:11 +0100] rev 62340
removed obsolete RC tags;
.hgtags

23 months ago wenzelm [Wed, 17 Feb 2016 21:06:47 +0100] rev 62339
merged
Admin/exec_process/build Admin/exec_process/etc/settings Admin/exec_process/exec_process.c src/HOL/Datatype_Examples/Brackin.thy src/HOL/Datatype_Examples/IsaFoR.thy src/HOL/Datatype_Examples/Misc_N2M.thy src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy src/HOL/Record_Benchmark/Record_Benchmark.thy

23 months ago wenzelm [Wed, 17 Feb 2016 15:57:10 +0100] rev 62338
Added tag Isabelle2016 for changeset d3996d5873dd
.hgtags