Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. clarified: constructors in the sense of the code generator are not invertible; correct treatment of constructors with same name but different type; moved doubtful comment to corresponding function call
  2. moved
Changeset 62581:fc5198b44314 by haftmann:
clarified: constructors in the sense of the code generator are not invertible;<br>correct treatment of constructors with same name but different type;<br>moved doubtful comment to corresponding function call
The file was modified src/HOL/Tools/Predicate_Compile/mode_inference.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML (diff)
Changeset 62580:7011429f44f9 by haftmann:
moved
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/String.thy (diff)