Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. restored test_code for GHC, which got accidentally broken in ef02c5e051e5
  2. restored quickcheck/narrowing, which got accidentally broken in ef02c5e051e5
  3. optional code export as theory export
  4. explicit model concerning files of generated code
Changeset 69626:0631421c6d6a by haftmann:
restored test_code for GHC, which got accidentally broken in ef02c5e051e5
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 69625:94048eac7463 by haftmann:
restored quickcheck/narrowing, which got accidentally broken in ef02c5e051e5
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
Changeset 69624:e02bdf853a4c by haftmann:
optional code export as theory export
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
The file was modified src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 69623:ef02c5e051e5 by haftmann:
explicit model concerning files of generated code
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/Tools/Code/code_haskell.ML (diff)
The file was modified src/Tools/Code/code_ml.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/Code/code_scala.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)