Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. more informative Spec_Rules.Equational: support corecursion;
  3. more operations;
  4. more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
Changeset 69997:9c634887be9e by wenzelm:
merged
Changeset 69996:8f2d3a27aff0 by wenzelm:
more informative Spec_Rules.Equational: support corecursion;
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 69995:2d5c313e8582 by wenzelm:
more operations;
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 69994:cf7150ab1075 by paulson _lp15@cam.ac.uk_:
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
The file was addedsrc/HOL/Analysis/Abstract_Euclidean_Space.thy
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Product_Topology.thy (diff)
The file was modified src/HOL/Analysis/T1_Spaces.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)