Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. suppress record types: not working properly;
  3. removed junk;
  4. discontinued somewhat pointless options;
  5. tuned signature;
  6. clarified signature;
  7. export datatypes;
  8. clarified modules;
  9. misc tuning and clarification: proper check of datatype kind;
  10. clarified modules;
  11. cleaning
  12. tuned
Changeset 71254:a9ad4a954cb7 by wenzelm:
merged
Changeset 71253:a62431901140 by wenzelm:
suppress record types: not working properly;
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
Changeset 71252:c5914bdd896b by wenzelm:
removed junk;
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
Changeset 71251:297d24fb262c by wenzelm:
discontinued somewhat pointless options;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 71250:bd93c71521a0 by wenzelm:
tuned signature;
The file was modified src/Pure/Concurrent/par_exn.ML (diff)
The file was modified src/Pure/ML/exn_properties.ML (diff)
Changeset 71249:877316c54ed3 by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 71248:adf5e53d2b2b by wenzelm:
export datatypes;
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 71247:6e0ff949073e by wenzelm:
clarified modules;
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
Changeset 71246:30db0523f9b0 by wenzelm:
misc tuning and clarification: proper check of datatype kind;
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
Changeset 71245:e5664a75f4b5 by wenzelm:
clarified modules;
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
Changeset 71244:38457af660bc by nipkow:
cleaning
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 71243:5b7c85586eb1 by nipkow:
tuned
The file was modified src/HOL/Analysis/Affine.thy (diff)