Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. state monad
  2. State_Monad ~> Open_State_Syntax
  3. more material on fmaps
  4. canonical representation for fmaps is fmlookup
  5. fmaps are countable
  6. merged
  7. card_0_eq ~> fcard_0_eq
  8. material from $AFP/Formula_Derivatives/FSet_More
  9. FSet is monadic
  10. finite sets are countable
  11. lift sum to finite sets
Changeset 66271:d157195a468a by lars hupel _lars.hupel@mytum.de_:
state monad
The file was addedsrc/HOL/Library/State_Monad.thy
The file was modified src/HOL/Library/Library.thy (diff)
Changeset 66270:403d84138c5c by lars hupel _lars.hupel@mytum.de_:
State_Monad ~> Open_State_Syntax
The file was addedsrc/HOL/Library/Open_State_Syntax.thy
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Proofs/Extraction/Higman_Extraction.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Library/State_Monad.thy
Changeset 66269:0820c8368320 by lars hupel _lars.hupel@mytum.de_:
more material on fmaps
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 66268:e4b98cad5ab4 by lars hupel _lars.hupel@mytum.de_:
canonical representation for fmaps is fmlookup
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 66267:04b626416eae by lars hupel _lars.hupel@mytum.de_:
fmaps are countable
The file was modified src/HOL/Library/Finite_Map.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
Changeset 66266:130dea8500cb by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 66265:a51e72d79670 by lars hupel _lars.hupel@mytum.de_:
card_0_eq ~> fcard_0_eq
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 66264:d516da3e7c42 by lars hupel _lars.hupel@mytum.de_:
material from $AFP/Formula_Derivatives/FSet_More
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 66263:466d8e7ed170 by lars hupel _lars.hupel@mytum.de_:
FSet is monadic
The file was modified src/HOL/Library/Monad_Syntax.thy (diff)
Changeset 66262:4a2c9d32e7aa by lars hupel _lars.hupel@mytum.de_:
finite sets are countable
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
Changeset 66261:fb6efe575c6d by lars hupel _lars.hupel@mytum.de_:
lift sum to finite sets
The file was modified src/HOL/Library/FSet.thy (diff)