Skip to content
Failed

Changes

Summary

  1. tuned signature;
  2. recover original order;
  3. tuned;
  4. misc tuning and modernization;
  5. merged
  6. clarified signature;
  7. clarified signature: more general types;
  8. afford redundant whitespace for improved readability;
  9. avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
Changeset 69869:f2c3512df446 by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/document_structure.scala (diff)
Changeset 69868:ab993a273def by wenzelm:
recover original order;
The file was modified src/Pure/General/rdf.scala (diff)
Changeset 69867:3fd9298dd200 by wenzelm:
tuned;
The file was modified src/Pure/General/pretty.scala (diff)
The file was modified src/Pure/General/rdf.scala (diff)
The file was modified src/Pure/PIDE/prover.scala (diff)
The file was modified src/Pure/PIDE/xml.scala (diff)
Changeset 69866:01732226987a by wenzelm:
misc tuning and modernization;
The file was modified src/FOL/ex/Nat.thy (diff)
The file was modified src/FOL/ex/Nat_Class.thy (diff)
Changeset 69865:c28da0820b8b by wenzelm:
merged
Changeset 69864:d594997cdcf4 by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/document_status.scala (diff)
The file was modified src/Tools/jEdit/src/timing_dockable.scala (diff)
Changeset 69863:9532d5b2e932 by wenzelm:
clarified signature: more general types;
The file was modified src/Pure/PIDE/document_status.scala (diff)
The file was modified src/Tools/jEdit/src/timing_dockable.scala (diff)
Changeset 69862:db622ada496d by wenzelm:
afford redundant whitespace for improved readability;
The file was modified src/Pure/General/rdf.scala (diff)
Changeset 69861:62e47f06d22c by haftmann:
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Integral_Substitution.thy (diff)
The file was modified src/HOL/Analysis/Measurable.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
The file was modified src/HOL/Library/Option_ord.thy (diff)
The file was modified src/HOL/Library/Order_Continuity.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
The file was modified src/HOL/Predicate.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Probability/Helly_Selection.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)