mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
10 lines
187 B
Plaintext
10 lines
187 B
Plaintext
theory Test
|
|
use bool.Bool
|
|
|
|
goal G1 : True <> False
|
|
goal G2 : forall x:bool. x = True \/ x = False
|
|
goal G3 : forall x y z:bool. x<>y /\ y<>z /\ z<>x -> false
|
|
|
|
end
|
|
|