Jump to content

Talk:Isabelle (proof assistant)

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia
This is the current revision of this page, as edited by Cewbot (talk | contribs) at 00:50, 4 February 2024 (Maintain {{WPBS}} and vital articles: 2 WikiProject templates. Create {{WPBS}}. Keep majority rating "Start" in {{WPBS}}. Remove 2 same ratings as {{WPBS}} in {{WikiProject Computer science}}, {{Maths rating}}. Remove 1 deprecated parameter: field.). The present address (URL) is a permanent link to this version.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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]