mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
12 lines
139 B
Plaintext
12 lines
139 B
Plaintext
theory HelloProof
|
|
|
|
goal G1: true
|
|
|
|
goal G2: (true -> false) /\ (true \/ false)
|
|
|
|
use int.Int
|
|
|
|
goal G3: forall x:int. x * x >= 0
|
|
|
|
end
|