Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more structural integrity;
  2. tuned;
  3. more structural integrity;
  4. clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
  5. tuned;
  6. clarified signature;
  7. tuned whitespace;
  8. clarified context: prefer abstract Variable.auto_fixes;
  9. tuned;
  10. tuned signature;
  11. redundant: default is false;
Changeset 70313:9c19e15c8548 by wenzelm:
more structural integrity;
The file was modified src/Pure/assumption.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70312:56f96489478c by wenzelm:
tuned;
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
Changeset 70311:e49bf4ebf330 by wenzelm:
more structural integrity;
The file was modified src/Pure/variable.ML (diff)
Changeset 70310:c82f59c47aaf by wenzelm:
clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;
The file was modified src/Pure/morphism.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70309:f9fd15d3cfac by wenzelm:
tuned;
The file was modified src/Pure/Isar/class_declaration.ML (diff)
Changeset 70308:7f568724d67e by wenzelm:
clarified signature;
The file was modified src/HOL/Decision_Procs/approximation.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Real_Asymp/real_asymp_diag.ML (diff)
The file was modified src/HOL/Tools/Function/fun_cases.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/code_prolog.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/exhaustive_generators.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
The file was modified src/HOL/Tools/functor.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/HOL/Tools/value_command.ML (diff)
The file was modified src/HOL/ex/Commands.thy (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
The file was modified src/Pure/variable.ML (diff)
Changeset 70307:53d21039518a by wenzelm:
tuned whitespace;
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 70306:61621dc439d4 by wenzelm:
clarified context: prefer abstract Variable.auto_fixes;
The file was modified src/Pure/Isar/local_defs.ML (diff)
Changeset 70305:959e167798f0 by wenzelm:
tuned;
The file was modified src/Pure/Isar/local_defs.ML (diff)
Changeset 70304:1514efa1e57a by wenzelm:
tuned signature;
The file was modified src/Doc/more_antiquote.ML (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/variable.ML (diff)
Changeset 70303:502749883f53 by wenzelm:
redundant: default is false;
The file was modified src/HOL/Import/import_rule.ML (diff)