Summary
- additional lemmas for State_Monad, courtesy of Andreas Lochbihler
- more material on finite maps
- redundant since c6714a9562ae
- store the unfolded definitions of the lifted bnf constants under "_def" name
The file was modified | src/HOL/Library/State_Monad.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/Tools/BNF/bnf_def.ML (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_lift.ML (diff) |