Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. deleting a code equation never leads to unimplemented function
  2. avoid ancient [code, code del] antipattern
  3. obsolete
  4. register equations stemming from extracted proofs as specification rules
  5. tuned
Changeset 66149:4bf16fb7c14d by haftmann:
deleting a code equation never leads to unimplemented function
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 66148:5e60c2d0a1f1 by haftmann:
avoid ancient [code, code del] antipattern
The file was modified src/HOL/Imperative_HOL/Heap_Monad.thy (diff)
The file was modified src/HOL/Library/Code_Binary_Nat.thy (diff)
The file was modified src/HOL/Library/Code_Real_Approx_By_Float.thy (diff)
The file was modified src/HOL/Library/DAList_Multiset.thy (diff)
The file was modified src/HOL/Library/RBT_Set.thy (diff)
The file was modified src/HOL/Quickcheck_Narrowing.thy (diff)
The file was modified src/HOL/Unix/Nested_Environment.thy (diff)
Changeset 66147:9225370db5f0 by haftmann:
obsolete
The file was modified src/HOL/Library/Code_Real_Approx_By_Float.thy (diff)
Changeset 66146:fd3e128b174f by haftmann:
register equations stemming from extracted proofs as specification rules
The file was modified src/Pure/Proof/extraction.ML (diff)
Changeset 66145:4efbcc308ca0 by haftmann:
tuned
The file was modified src/Pure/Proof/extraction.ML (diff)