Summary
- merged
- drop redundant fundef_cong rule
- tuned
- repair malformed fundef_cong rule
The file was modified | src/HOL/Fun_Def.thy (diff) |
The file was modified | src/HOL/Data_Structures/Binomial_Heap.thy (diff) |
The file was modified | src/HOL/Probability/Probability_Mass_Function.thy (diff) |
The file was modified | src/HOL/Library/Finite_Map.thy (diff) |