6 months ago Andreas Lochbihler [Tue, 01 Jan 2019 17:04:53 +0100] rev 69568
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
CONTRIBUTORS NEWS src/HOL/Library/Simps_Case_Conv.thy src/HOL/Library/case_converter.ML src/HOL/Library/code_lazy.ML src/HOL/Library/simps_case_conv.ML src/HOL/ex/Simps_Case_Conv_Examples.thy

6 months ago Andreas Lochbihler [Sun, 30 Dec 2018 10:30:41 +0100] rev 69567
separate case converter into a separate theory
src/HOL/Library/Case_Converter.thy src/HOL/Library/Code_Lazy.thy

6 months ago wenzelm [Tue, 01 Jan 2019 21:47:27 +0100] rev 69566
more antiquotations -- less LaTeX macros;
src/HOL/Analysis/Ball_Volume.thy src/HOL/Analysis/Binary_Product_Measure.thy src/HOL/Analysis/Bochner_Integration.thy src/HOL/Analysis/Borel_Space.thy src/HOL/Analysis/Brouwer_Fixpoint.thy src/HOL/Analysis/Complete_Measure.thy src/HOL/Analysis/Complex_Transcendental.thy src/HOL/Analysis/Embed_Measure.thy src/HOL/Analysis/Extended_Real_Limits.thy src/HOL/Analysis/Function_Topology.thy src/HOL/Analysis/Further_Topology.thy src/HOL/Analysis/Gamma_Function.thy src/HOL/Analysis/Lipschitz.thy src/HOL/Analysis/Measure_Space.thy src/HOL/Analysis/Path_Connected.thy src/HOL/Analysis/Set_Integral.thy src/HOL/Analysis/Sigma_Algebra.thy

6 months ago wenzelm [Tue, 01 Jan 2019 20:57:54 +0100] rev 69565
retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
src/HOL/Analysis/Continuum_Not_Denumerable.thy src/HOL/Analysis/Infinite_Products.thy src/HOL/Analysis/Norm_Arith.thy src/HOL/Analysis/Path_Connected.thy src/HOL/Analysis/Tagged_Division.thy

6 months ago nipkow [Tue, 01 Jan 2019 13:26:37 +0100] rev 69564
tuned defs
src/HOL/Analysis/Elementary_Topology.thy src/HOL/Analysis/Measure_Space.thy

6 months ago wenzelm [Mon, 31 Dec 2018 22:21:34 +0100] rev 69563
merged

6 months ago wenzelm [Mon, 31 Dec 2018 22:21:02 +0100] rev 69562
include loaded_files as doc_blobs (without purging);
src/Pure/PIDE/headless.scala

6 months ago wenzelm [Mon, 31 Dec 2018 21:12:22 +0100] rev 69561
tuned signature;
src/Pure/PIDE/resources.scala

6 months ago wenzelm [Mon, 31 Dec 2018 20:13:36 +0100] rev 69560
clarified signature;
src/Pure/PIDE/resources.scala src/Pure/Thy/sessions.scala

6 months ago wenzelm [Mon, 31 Dec 2018 20:08:32 +0100] rev 69559
tuned;
src/Pure/Thy/thy_syntax.scala