Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. tuned;
  2. tuned;
  3. backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
  4. unused;
  5. tuned messages;
  6. proper context;
  7. misc tuning and clarification, notably wrt. flow of context;
  8. proper context;
  9. proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
  10. unused;
  11. misc tuning and clarification, notably wrt. flow of context;
  12. proper context;
  13. proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
Changeset 70326:aa7c49651f4e by wenzelm:
tuned;
The file was modified src/HOL/HOL.thy
The file was modified src/HOL/Library/Cancellation/cancel.ML
The file was modified src/HOL/Nominal/nominal_inductive.ML
The file was modified src/HOL/Nominal/nominal_inductive2.ML
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
The file was modified src/HOL/Tools/Function/function_common.ML
The file was modified src/HOL/Tools/Meson/meson_clausify.ML
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
The file was modified src/HOL/Tools/set_comprehension_pointfree.ML
The file was modified src/Provers/Arith/cancel_numeral_factor.ML
The file was modified src/Provers/Arith/cancel_numerals.ML
The file was modified src/Provers/Arith/combine_numerals.ML
The file was modified src/Provers/Arith/extract_common_term.ML
The file was modified src/Pure/Thy/document_antiquotations.ML
Changeset 70325:9bf04a8f211f by wenzelm:
tuned;
The file was modified src/HOL/Tools/Function/partial_function.ML
Changeset 70324:005c1cdbfd3f by wenzelm:
backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
The file was modified src/HOL/Tools/Function/partial_function.ML
Changeset 70323:2943934a169d by wenzelm:
unused;
The file was modified src/HOL/Tools/Lifting/lifting_util.ML
Changeset 70322:65b880d4efbb by wenzelm:
tuned messages;
The file was modified src/HOL/Tools/Lifting/lifting_info.ML
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML
Changeset 70321:24877d539fb8 by wenzelm:
proper context;
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML
The file was modified src/HOL/Tools/Lifting/lifting_term.ML
Changeset 70320:59258a3192bf by wenzelm:
misc tuning and clarification, notably wrt. flow of context;
The file was modified src/HOL/Tools/Lifting/lifting_bnf.ML
The file was modified src/HOL/Tools/Lifting/lifting_def.ML
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML
The file was modified src/HOL/Tools/Lifting/lifting_info.ML
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML
The file was modified src/HOL/Tools/Lifting/lifting_term.ML
The file was modified src/HOL/Tools/Lifting/lifting_util.ML
The file was modified src/HOL/Tools/Meson/meson_clausify.ML
The file was modified src/HOL/Tools/SMT/smt_replay.ML
Changeset 70319:34bc296374ee by wenzelm:
proper context;
The file was modified src/HOL/Tools/Function/partial_function.ML
Changeset 70318:9eff9e2dc177 by wenzelm:
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
The file was modified src/HOL/Tools/Function/fun_cases.ML
The file was modified src/HOL/Tools/inductive.ML
Changeset 70317:9fced5690f4e by wenzelm:
unused;
The file was removedsrc/HOL/Tools/legacy_transfer.ML
Changeset 70316:c61b7af108a6 by wenzelm:
misc tuning and clarification, notably wrt. flow of context;
The file was modified src/HOL/Tools/Transfer/transfer.ML
The file was modified src/HOL/Tools/Transfer/transfer_bnf.ML
Changeset 70315:2f9623aa1eeb by wenzelm:
proper context;
The file was modified src/Provers/Arith/cancel_numeral_factor.ML
The file was modified src/Provers/Arith/cancel_numerals.ML
The file was modified src/Provers/Arith/combine_numerals.ML
The file was modified src/Provers/Arith/extract_common_term.ML
Changeset 70314:6d6839a948cf by wenzelm:
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
The file was modified src/Pure/Isar/expression.ML
The file was modified src/Pure/Isar/interpretation.ML
The file was modified src/Pure/Isar/local_defs.ML