src/HOL/Library/Imperative_HOL.thy
changeset 29120 8a904ff43f28
parent 27656 d4f6e64ee7cc
equal deleted inserted replaced
29119:99941fd0cb0e 29120:8a904ff43f28