changeset 136:db7c7871bea4

Removed the invariant from while-loop.py This one would be added explicitly in isabelle.
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 04 Nov 2009 14:50:54 +0100
parents 16f4be0b0e9a
children 2f8f9b0013d5
files examples/while-loop.py
diffstat 1 files changed, 0 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/examples/while-loop.py	Wed Nov 04 14:28:59 2009 +0100
+++ b/examples/while-loop.py	Wed Nov 04 14:50:54 2009 +0100
@@ -9,7 +9,6 @@
     low = 0
     high = len(bids)
     while(low < high):
-        invariant("bids[high] >= 0 and 0 >= bids[low]")
         mid = (low + high) // 2
         r = open(bids[mid] >= 0)
         if r: