Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. merged
  3. new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
  4. separate case converter into a separate theory
  5. more antiquotations -- less LaTeX macros;
  6. retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
  7. tuned defs
Changeset 69570:2f78e0d73a34 by Andreas Lochbihler:
merged
Changeset 69569:2d88bf80c84f by Andreas Lochbihler:
merged
Changeset 69568:de09a7261120 by Andreas Lochbihler:
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Simps_Case_Conv.thy (diff)
The file was modified src/HOL/Library/case_converter.ML (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/Library/simps_case_conv.ML (diff)
The file was modified src/HOL/ex/Simps_Case_Conv_Examples.thy (diff)
Changeset 69567:6b4c41037649 by Andreas Lochbihler:
separate case converter into a separate theory
The file was addedsrc/HOL/Library/Case_Converter.thy
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
Changeset 69566:c41954ee87cf by wenzelm:
more antiquotations -- less LaTeX macros;
The file was modified src/HOL/Analysis/Ball_Volume.thy (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Embed_Measure.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Lipschitz.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
Changeset 69565:1daf07b65385 by wenzelm:
retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
The file was modified src/HOL/Analysis/Continuum_Not_Denumerable.thy (diff)
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
The file was modified src/HOL/Analysis/Norm_Arith.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
Changeset 69564:a59f7d07bf17 by nipkow:
tuned defs
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)