Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned;
  3. more antiquotations;
  4. more antiquotations;
  5. more robust: genuinely free variables need to be instantiated;
  6. tuned comments;
  7. clarified errors;
  8. tuned;
  9. clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
  10. tuned;
  11. clarified signature -- avoid clones;
  12. Refinement of partitions
Changeset 74585:42fb56041c11 by wenzelm:
merged
Changeset 74584:c14787d73db6 by wenzelm:
tuned;
The file was modified src/Doc/Codegen/Computations.thy (diff)
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
The file was modified src/HOL/ex/Sorting_Algorithms_Examples.thy (diff)
Changeset 74583:0eb2f18b1806 by wenzelm:
more antiquotations;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74582:882de99c7c83 by wenzelm:
more antiquotations;
The file was modified src/Doc/Codegen/Computations.thy (diff)
The file was modified src/HOL/ex/Sorting_Algorithms_Examples.thy (diff)
Changeset 74581:e5b38bb5a147 by wenzelm:
more robust: genuinely free variables need to be instantiated;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74580:d114553793df by wenzelm:
tuned comments;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74579:bf703bfc065c by wenzelm:
clarified errors;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
Changeset 74578:9bfbb5f7ec99 by wenzelm:
tuned;
The file was modified src/Pure/term_subst.ML (diff)
Changeset 74577:d4829a7333e2 by wenzelm:
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/term.ML (diff)
The file was modified src/Pure/term_subst.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 74576:0b43d42cfde7 by wenzelm:
tuned;
The file was modified src/Pure/term_subst.ML (diff)
Changeset 74575:ccf599864beb by wenzelm:
clarified signature -- avoid clones;
The file was modified src/HOL/Tools/BNF/bnf_comp.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML (diff)
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/envir.ML (diff)
Changeset 74574:cff477b6d015 by paulson _lp15@cam.ac.uk_:
Refinement of partitions
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)