summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Check.ssc
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-07-09 03:10:43 +0000
committerGravatar rustanleino <unknown>2010-07-09 03:10:43 +0000
commit442dceca5acb9ab93978d0173e850125288db6d5 (patch)
treecd499b781719736bbec692b2339623e6a5c46eb0 /Source/VCGeneration/Check.ssc
parenta751d6ada517ee4edeeee476e319c52e4d3388da (diff)
Dafny: Axiom about inverting a set union operation, similar to the recent ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
Diffstat (limited to 'Source/VCGeneration/Check.ssc')
0 files changed, 0 insertions, 0 deletions