Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. tuned signature;
  3. tuned signature;
  4. tuned signature;
  5. removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq;
  6. prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;
  7. added HOLogic.mk_obj_eq convenience and eliminated some clones;
  8. tuned -- use existing Morphism.instantiate_morphism;
Changeset 67716:3f611f444c2d by wenzelm:
merged
Changeset 67715:ec46ecb87999 by wenzelm:
tuned signature;
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
Changeset 67714:a0b58be402ab by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 67713:041898537c19 by wenzelm:
tuned signature;
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_datatype_aux.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_rep_datatype.ML (diff)
The file was modified src/Pure/Isar/expression.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/global_theory.ML (diff)
Changeset 67712:350f0579d343 by wenzelm:
removed unused clone of (map o apsnd);<br>removed unused variant of HOLogic.mk_obj_eq;
The file was modified src/HOL/Tools/Lifting/lifting_util.ML (diff)
Changeset 67711:951f96d386cf by wenzelm:
prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;
The file was modified src/HOL/Tools/groebner.ML (diff)
Changeset 67710:cc2db3239932 by wenzelm:
added HOLogic.mk_obj_eq convenience and eliminated some clones;
The file was modified src/Doc/more_antiquote.ML (diff)
The file was modified src/HOL/Decision_Procs/Conversions.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Nominal/nominal_permeq.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
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_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Function/function_context_tree.ML (diff)
The file was modified src/HOL/Tools/Function/function_core.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_util.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/cnf.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/set_comprehension_pointfree.ML (diff)
The file was modified src/HOL/Tools/simpdata.ML (diff)
Changeset 67709:3c9e0b4709e7 by wenzelm:
tuned -- use existing Morphism.instantiate_morphism;
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_util.ML (diff)