Skip to content
Success

Changes

Summary

  1. De-applied Ideal.thy
  2. material on finite sets and maps
  3. simplify parametricity proofs
  4. merged
  5. added simp rules
Changeset 68464:3ead36cbe6b7 by paulson _lp15@cam.ac.uk_:
De-applied Ideal.thy
The file was modified src/HOL/Algebra/Ideal.thy (diff)
Changeset 68463:410818a69ee3 by lars hupel _lars.hupel@mytum.de_:
material on finite sets and maps
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)
Changeset 68462:8d1bf38c6fe6 by lars hupel _lars.hupel@mytum.de_:
simplify parametricity proofs
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 68461:8dea233d4bae by nipkow:
merged
Changeset 68460:b047339bd11c by nipkow:
added simp rules
The file was modified src/HOL/Map.thy (diff)
The file was modified src/HOL/Option.thy (diff)