Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. Merge
  2. lemmas about dimension, hyperplanes, span, etc.
  3. merged
  4. clarified context, notably for internal use of Simplifier;
Changeset 63076:1e771f0db448 by paulson _lp15@cam.ac.uk_:
Merge
Changeset 63075:60a42a4166af by paulson _lp15@cam.ac.uk_:
lemmas about dimension, hyperplanes, span, etc.
The file was modified src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Determinants.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63074:c60730295599 by wenzelm:
merged
Changeset 63073:413184c7a2a2 by wenzelm:
clarified context, notably for internal use of Simplifier;
The file was modified src/Doc/more_antiquote.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Tools/Code/code_preproc.ML (diff)
The file was modified src/Tools/Code/code_thingol.ML (diff)