Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned signature
  2. more correct exception handling
  3. explicit tagging of code equations de-baroquifies interface
  4. dropped unused code
  5. conventional syntax for unit abstractions
Changeset 63241:f59fd6cc935e by haftmann:
tuned signature
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 63240:f82c0b803bda by haftmann:
more correct exception handling
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 63239:d562c9948dee by haftmann:
explicit tagging of code equations de-baroquifies interface
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/HOL/Library/Mapping.thy (diff)
The file was modified src/HOL/Library/old_recdef.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_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_compat.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.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.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_primrec.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_rep_datatype.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_size.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/code_evaluation.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
Changeset 63238:7c593d4f1f89 by haftmann:
dropped unused code
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 63237:3e908f762817 by haftmann:
conventional syntax for unit abstractions
The file was modified NEWS (diff)
The file was modified src/HOL/Product_Type.thy (diff)