10 months ago nipkow [Sun, 17 Jun 2018 20:31:51 +0200] rev 68460
added simp rules
src/HOL/Map.thy src/HOL/Option.thy

10 months ago paulson [Sun, 17 Jun 2018 22:01:16 +0100] rev 68459
merged

10 months ago paulson <lp15@cam.ac.uk> [Sun, 17 Jun 2018 22:00:43 +0100] rev 68458
Algebra tidy-up
src/HOL/Algebra/FiniteProduct.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/Ideal.thy src/HOL/Number_Theory/Residues.thy

10 months ago nipkow [Sun, 17 Jun 2018 13:10:14 +0200] rev 68457
added simp rule
src/HOL/Product_Type.thy

10 months ago nipkow [Sat, 16 Jun 2018 22:09:24 +0200] rev 68456
more simp
src/HOL/Transitive_Closure.thy

10 months ago nipkow [Sat, 16 Jun 2018 20:32:00 +0200] rev 68455
moved lemmas from AFP
src/HOL/Relation.thy src/HOL/Transitive_Closure.thy

10 months ago nipkow [Sat, 16 Jun 2018 07:13:17 +0200] rev 68454
moved lemmas from AFP
src/HOL/Map.thy

10 months ago paulson [Fri, 15 Jun 2018 13:52:05 +0100] rev 68453
merged

10 months ago paulson <lp15@cam.ac.uk> [Fri, 15 Jun 2018 12:18:06 +0100] rev 68452
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
src/HOL/Algebra/Coset.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/Zassenhaus.thy src/HOL/Analysis/Infinite_Products.thy

10 months ago nipkow [Fri, 15 Jun 2018 13:02:12 +0200] rev 68451
empty -> Map.empty
src/HOL/Bali/AxCompl.thy src/HOL/Bali/AxSem.thy src/HOL/Bali/AxSound.thy src/HOL/Bali/Conform.thy src/HOL/Bali/DeclConcepts.thy src/HOL/Bali/DefiniteAssignmentCorrect.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy src/HOL/Bali/Example.thy src/HOL/Bali/State.thy src/HOL/Bali/Table.thy src/HOL/Bali/TypeSafe.thy src/HOL/Bali/WellForm.thy src/HOL/Hoare/Separation.thy src/HOL/IMP/Fold.thy src/HOL/MicroJava/Comp/AuxLemmas.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/Comp/DefsComp.thy src/HOL/MicroJava/J/Example.thy src/HOL/MicroJava/J/Exceptions.thy src/HOL/MicroJava/J/JListExample.thy src/HOL/MicroJava/J/TypeRel.thy src/HOL/MicroJava/J/WellForm.thy src/HOL/NanoJava/Example.thy src/HOL/NanoJava/State.thy src/HOL/NanoJava/TypeRel.thy src/HOL/Unix/Unix.thy