Summary
- 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
- moved
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) |
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/String.thy (diff) |