Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid Local_Theory.reset in application space
  2. tuned
  3. specific output setup is not supposed to intrude regular import theory
  4. avoid duplicate
  5. streamlined code setup for fake terms
  6. modernized (code) setup for enumeration predicates
  7. simplified setup
  8. executable domain membership checks
Changeset 66017:57acac0fd29b by haftmann:
avoid Local_Theory.reset in application space
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
Changeset 66016:39d9a59d8d94 by haftmann:
tuned
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
Changeset 66015:70643edecb7a by haftmann:
specific output setup is not supposed to intrude regular import theory
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 66014:2f45f4abf0a9 by haftmann:
avoid duplicate
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
Changeset 66013:03002d10bf1d by haftmann:
streamlined code setup for fake terms
The file was modified src/HOL/Code_Evaluation.thy (diff)
Changeset 66012:59bf29d2b3a1 by haftmann:
modernized (code) setup for enumeration predicates
The file was modified src/HOL/Predicate.thy (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML (diff)
Changeset 66011:f10bbfe07c41 by haftmann:
simplified setup
The file was modified src/HOL/Nitpick.thy (diff)
Changeset 66010:2f7d39285a1a by haftmann:
executable domain membership checks
The file was modified src/HOL/Map.thy (diff)