Summary
- State_Monad ~> Open_State_Syntax
- more material on fmaps
- canonical representation for fmaps is fmlookup
- fmaps are countable
The file was added | src/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 removed | src/HOL/Library/State_Monad.thy |
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/Library/Finite_Map.thy (diff) |
The file was modified | src/HOL/Probability/Fin_Map.thy (diff) |