10 lines
155 B
Text
10 lines
155 B
Text
theory HelloProof
|
|
goal G1: true
|
|
goal G4: false
|
|
goal G2: (true -> true) /\ (true \/ false)
|
|
use int.Int
|
|
goal G3: forall x:int. x * x >= 0
|
|
|
|
|
|
end
|
|
|