2. Natural Deduction and Starting with Isabelle

Question 1

What is the basic structrue of an isabelle .thy file?

Answer 1

theory MyTheory
imports T1 ... Tn
begin
(definitions, theorems, proofs, ...)*
end

MyTheory is the name of the theory

T1 .. Tn are imported theories