2 hours ago blanchet [Fri, 20 Jul 2018 22:19:42 +0200] rev 68668 default tip
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

14 hours ago Andreas Lochbihler [Fri, 20 Jul 2018 10:09:59 +0200] rev 68667
add lemmas about prod_filter
src/HOL/Filter.thy

15 hours ago paulson [Fri, 20 Jul 2018 09:05:34 +0200] rev 68666
merged

23 hours ago paulson <lp15@cam.ac.uk> [Fri, 20 Jul 2018 00:32:10 +0200] rev 68665
corrections to markup
src/HOL/Algebra/Ring_Divisibility.thy

25 hours ago paulson <lp15@cam.ac.uk> [Thu, 19 Jul 2018 23:23:10 +0200] rev 68664
updated material concerning Algebra
src/HOL/Algebra/Divisibility.thy src/HOL/Algebra/Generated_Rings.thy src/HOL/Algebra/Polynomials.thy src/HOL/Algebra/RingHom.thy src/HOL/Algebra/Ring_Divisibility.thy src/HOL/Algebra/Subrings.thy

30 hours ago paulson [Thu, 19 Jul 2018 17:28:13 +0200] rev 68663
merged

30 hours ago paulson <lp15@cam.ac.uk> [Thu, 19 Jul 2018 17:27:44 +0200] rev 68662
de-applying
src/HOL/Algebra/Group.thy src/HOL/Real.thy

21 hours ago wenzelm [Fri, 20 Jul 2018 03:14:44 +0200] rev 68661
added system option "strict_facts";
NEWS etc/options src/Pure/Isar/proof_context.ML src/Pure/global_theory.ML

2 days ago haftmann [Wed, 18 Jul 2018 20:51:23 +0200] rev 68660
slightly more canonical imports
src/HOL/Library/Lattice_Syntax.thy src/HOL/Quotient_Examples/Quotient_Int.thy src/HOL/ex/Computations.thy

2 days ago haftmann [Wed, 18 Jul 2018 20:51:22 +0200] rev 68659
setup for Haskell taken over from AFP / Gauss_Jordan
src/HOL/Library/IArray.thy