src/LK/lk.thy
changeset 4525 b96b513c6c65
parent 283 76caebd18756