Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. clarified signature;
Changeset 10443:7149dd204040 by wenzelm:
clarified signature;
The file was modified thys/Applicative_Lifting/applicative.ML
The file was modified thys/Auto2_HOL/HOL/matcher_test.ML
The file was modified thys/Auto2_HOL/HOL/rewrite_test.ML
The file was modified thys/Auto2_Imperative_HOL/Imperative/list_matcher_test.ML
The file was modified thys/Auto2_Imperative_HOL/Imperative/sep_steps_test.ML
The file was modified thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy
The file was modified thys/IMP2/automation/IMP2_Var_Abs.thy
The file was modified thys/Nominal2/nominal_dt_quot.ML
The file was modified thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

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
The file was modified src/Pure/thm.ML
Changeset 70312:56f96489478c by wenzelm:
tuned;
The file was modified src/HOL/Tools/Function/function_common.ML
Changeset 70311:e49bf4ebf330 by wenzelm:
more structural integrity;
The file was modified src/Pure/variable.ML
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
The file was modified src/Pure/thm.ML
Changeset 70309:f9fd15d3cfac by wenzelm:
tuned;
The file was modified src/Pure/Isar/class_declaration.ML
Changeset 70308:7f568724d67e by wenzelm:
clarified signature;
The file was modified src/HOL/Decision_Procs/approximation.ML
The file was modified src/HOL/Library/old_recdef.ML
The file was modified src/HOL/Real_Asymp/real_asymp_diag.ML
The file was modified src/HOL/Tools/Function/fun_cases.ML
The file was modified src/HOL/Tools/Predicate_Compile/code_prolog.ML
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
The file was modified src/HOL/Tools/Quickcheck/exhaustive_generators.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
The file was modified src/HOL/Tools/functor.ML
The file was modified src/HOL/Tools/inductive.ML
The file was modified src/HOL/Tools/semiring_normalizer.ML
The file was modified src/HOL/Tools/value_command.ML
The file was modified src/HOL/ex/Commands.thy
The file was modified src/Pure/Isar/element.ML
The file was modified src/Pure/Isar/expression.ML
The file was modified src/Pure/Isar/isar_cmd.ML
The file was modified src/Pure/Isar/local_defs.ML
The file was modified src/Pure/Isar/proof.ML
The file was modified src/Pure/Isar/proof_context.ML
The file was modified src/Pure/Isar/specification.ML
The file was modified src/Pure/Thy/document_antiquotations.ML
The file was modified src/Pure/Thy/thy_output.ML
The file was modified src/Pure/simplifier.ML
The file was modified src/Pure/variable.ML
Changeset 70307:53d21039518a by wenzelm:
tuned whitespace;
The file was modified src/Pure/Isar/proof_context.ML
Changeset 70306:61621dc439d4 by wenzelm:
clarified context: prefer abstract Variable.auto_fixes;
The file was modified src/Pure/Isar/local_defs.ML
Changeset 70305:959e167798f0 by wenzelm:
tuned;
The file was modified src/Pure/Isar/local_defs.ML
Changeset 70304:1514efa1e57a by wenzelm:
tuned signature;
The file was modified src/Doc/more_antiquote.ML
The file was modified src/Pure/Isar/attrib.ML
The file was modified src/Pure/variable.ML
Changeset 70303:502749883f53 by wenzelm:
redundant: default is false;
The file was modified src/HOL/Import/import_rule.ML