Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. State_Monad ~> Open_State_Syntax
  2. more material on fmaps
  3. canonical representation for fmaps is fmlookup
  4. fmaps are countable
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)