11 months ago immler [Tue, 10 Jul 2018 09:38:35 +0200] rev 68607
make theorem, corollary, and proposition %important for HOL-Analysis manual
src/HOL/Analysis/Connected.thy src/HOL/Analysis/Continuous_Extension.thy src/HOL/Analysis/Continuum_Not_Denumerable.thy src/HOL/Analysis/Convex_Euclidean_Space.thy src/HOL/Analysis/L2_Norm.thy src/HOL/Analysis/Linear_Algebra.thy src/HOL/Analysis/Measure_Space.thy src/HOL/Analysis/Norm_Arith.thy src/HOL/Analysis/Path_Connected.thy src/HOL/Analysis/Product_Vector.thy src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Analysis/Starlike.thy src/HOL/Analysis/Topology_Euclidean_Space.thy src/HOL/ROOT

11 months ago paulson <lp15@cam.ac.uk> [Mon, 09 Jul 2018 21:55:40 +0100] rev 68606
removal of smt and certain refinements
src/HOL/Algebra/Chinese_Remainder.thy src/HOL/Algebra/Group_Action.thy src/HOL/Algebra/Ideal_Product.thy src/HOL/Computational_Algebra/Factorial_Ring.thy

11 months ago paulson <lp15@cam.ac.uk> [Sun, 08 Jul 2018 23:35:33 +0100] rev 68605
removal of smt
src/HOL/Algebra/Cycles.thy src/HOL/Algebra/Generated_Groups.thy src/HOL/Algebra/Group.thy src/HOL/Algebra/Ideal_Product.thy src/HOL/Algebra/Polynomials.thy src/HOL/Algebra/Solvable_Groups.thy src/HOL/Algebra/Zassenhaus.thy

11 months ago paulson <lp15@cam.ac.uk> [Sun, 08 Jul 2018 16:07:26 +0100] rev 68604
elimination of some "smt"
src/HOL/Algebra/Coset.thy src/HOL/Algebra/Divisibility.thy src/HOL/Algebra/Embedded_Algebras.thy src/HOL/Algebra/Ideal.thy src/HOL/Algebra/QuotRing.thy src/HOL/Algebra/Ring_Divisibility.thy src/HOL/Algebra/Sym_Groups.thy src/HOL/Algebra/Zassenhaus.thy

11 months ago paulson <lp15@cam.ac.uk> [Sun, 08 Jul 2018 11:00:20 +0100] rev 68603
De-applying
src/HOL/Transcendental.thy

11 months ago paulson [Sat, 07 Jul 2018 15:07:46 +0100] rev 68602
merged

11 months ago paulson <lp15@cam.ac.uk> [Sat, 07 Jul 2018 15:07:37 +0100] rev 68601
de-applying, etc.
src/HOL/Analysis/Weierstrass_Theorems.thy src/HOL/Deriv.thy src/HOL/Transcendental.thy

11 months ago nipkow [Fri, 06 Jul 2018 22:52:49 +0200] rev 68600
more symmetric
src/HOL/Data_Structures/Leftist_Heap.thy

11 months ago wenzelm [Fri, 06 Jul 2018 21:19:24 +0200] rev 68599
prefer HTTPS;
ANNOUNCE

11 months ago wenzelm [Fri, 06 Jul 2018 16:29:47 +0200] rev 68598
just one global lock for group status: avoid proliferation of mutexes, condvars;
src/Pure/Concurrent/task_queue.ML