Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified signature;
  2. more robust: client could have terminated already;
  3. clarified signature;
  4. clarified signature;
  5. clarified modules;
  6. clarified set of items with order of addition;
  7. tuned message;
  8. tuned whitespace;
  9. clarified signature; clarified modules;
  10. tuned;
  11. simplified: uniqueness check happens in export_consumer;
Changeset 74274:36f2c4a5c21b by wenzelm:
clarified signature;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
The file was modified src/HOL/Decision_Procs/ferrante_rackoff.ML (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
The file was modified src/HOL/Tools/Qelim/qelim.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
Changeset 74273:0a4cdf0036a0 by wenzelm:
more robust: client could have terminated already;
The file was modified src/Pure/System/bash.scala (diff)
Changeset 74272:0f3ca0cd8071 by wenzelm:
clarified signature;
The file was modified src/Pure/cterm_items.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
Changeset 74271:64be5f224462 by wenzelm:
clarified signature;
The file was modified src/Pure/cterm_items.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
Changeset 74270:ad2899cdd528 by wenzelm:
clarified modules;
The file was addedsrc/Pure/cterm_items.ML
The file was addedsrc/Pure/term_items.ML
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/conv.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 74269:f084d599bb44 by wenzelm:
clarified set of items with order of addition;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
The file was modified src/HOL/Decision_Procs/ferrante_rackoff.ML (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
The file was modified src/HOL/Tools/Qelim/qelim.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/Pure/General/table.ML (diff)
The file was modified src/Pure/Isar/obtain.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
Changeset 74268:d01920a8b082 by wenzelm:
tuned message;
The file was modified src/Pure/System/isabelle_system.scala (diff)
Changeset 74267:5c110ac28dcf by wenzelm:
tuned whitespace;
The file was modified src/Pure/Isar/subgoal.ML (diff)
Changeset 74266:612b7e0d6721 by wenzelm:
clarified signature;<br>clarified modules;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Doc/Implementation/Proof.thy (diff)
The file was modified src/HOL/Eisbach/match_method.ML (diff)
The file was modified src/HOL/Library/cconv.ML (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.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_gfp_rec_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML (diff)
The file was modified src/HOL/Tools/Function/induction_schema.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
The file was modified src/HOL/Tools/choice_specification.ML (diff)
The file was modified src/Pure/General/table.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/Isar/obtain.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Proof/proof_checker.ML (diff)
The file was modified src/Pure/Proof/proof_rewrite_rules.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/consts.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
The file was modified src/Pure/primitive_defs.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
The file was modified src/Pure/term_subst.ML (diff)
The file was modified src/Pure/theory.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/type.ML (diff)
The file was modified src/Pure/type_infer.ML (diff)
The file was modified src/Pure/variable.ML (diff)
The file was modified src/Tools/IsaPlanner/rw_inst.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
Changeset 74265:633fe7390c97 by wenzelm:
tuned;
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
Changeset 74264:04214caeb9ac by wenzelm:
simplified: uniqueness check happens in export_consumer;
The file was modified src/Pure/Thy/export_theory.ML (diff)