1 files changed, 0 insertions, 44 deletions
diff --git a/Jennisys/Jennisys/examples/Number.jen b/Jennisys/Jennisys/examples/Number.jen
deleted file mode 100644
index e31613bd..00000000
--- a/Jennisys/Jennisys/examples/Number.jen
+++ /dev/null
@@ -1,44 +0,0 @@
-interface Number { 
-  var num: int
- 
-  constructor Init(p: int)
-    ensures num = p
-
-  constructor Double(p: int)
-    ensures num = 2*p
-
-  constructor Sum(a: int, b: int)
-    ensures num = a + b
-
-  constructor Min2(a: int, b: int)
-    ensures a < b ==> num = a
-    ensures a >= b ==> num = b
-
-  constructor Min22(a: int, b: int)
-    ensures num in {a b}
-    ensures num <= a && num <= b
-
-  constructor Min3(a: int, b: int, c: int)
-    ensures num in {a b c}
-    ensures num <= a && num <= b && num <= c
-
-  constructor Min32(a: int, b: int, c: int)
-    ensures num in {a b c}
-    ensures forall x :: x in {a b c} ==> num <= x
-
-  constructor MinSum(a: int, b: int, c: int)
-    ensures num in {a+b a+c b+c}
-    ensures num <= a+b && num <= b+c && num <= a+c
-
-  constructor Min4(a: int, b: int, c: int, d: int)
-    ensures num in {a b c d}
-    ensures forall x :: x in {a b c d} ==> num <= x
-
-  constructor Abs(a: int)  
-    ensures num in {a (-a)} && num >= 0
-
-}
-
-datamodel Number {
-
-}
-\ No newline at end of file