Summary
- De-applied Ideal.thy
- material on finite sets and maps
- simplify parametricity proofs
- merged
- added simp rules
The file was modified | src/HOL/Algebra/Ideal.thy (diff) |
The file was modified | src/HOL/Finite_Set.thy (diff) |
The file was modified | src/HOL/Library/FSet.thy (diff) |
The file was modified | src/HOL/Library/Finite_Map.thy (diff) |
The file was modified | src/HOL/Library/Finite_Map.thy (diff) |
The file was modified | src/HOL/Map.thy (diff) |
The file was modified | src/HOL/Option.thy (diff) |