Edge Rewrite
Jump to content

Talk:Isabelle (proof assistant)

Page contents not supported in other languages.
Add topic
From Wikipedia, the free encyclopedia
Latest comment: 5 years ago by Sander123 in topic Untitled

Untitled

[edit]

To make the example compile, you need to save it in a file, say Sqrt2.thy, and add before the proof text, the statements:

theory Sqrt2

imports Complex_Main

begin

after the proof text one could add 'end'. Sander123 (talk) 11:16, 26 February 2021 (UTC)Reply