HomeIsabelle/Phabricator

Adjust Imperative List/Map/Set Specification for more lenient next operation

Description

Adjust Imperative List/Map/Set Specification for more lenient next operation

This allows implementations of this iterator specification to make use of
temporary variables for obtaining the next element of the list/set/map.
This is required by some and especially more general iterators.

Details