theory Test
  imports Main
begin

text \<open>If you are running Isabelle 2024, you should be able to load and process this file smoothly
  (in particular with the following line not being underlined with red squiggles).\<close>

thm even_half_succ_eq

text \<open>The above line just checks that Isabelle can find this lemma (and that you are running
  Isabelle 2024 or later;  in previous versions the lemma had a different name).

  If you put your cursor on that line and open the "Output" panel (at the bottom by default),
  Isabelle should print the lemma.\<close>

section \<open>Installing Isabelle\<close>

text \<open>Download Isabelle from \<^url>\<open>https://isabelle.in.tum.de/\<close> and follow the installation
  instructions for your operating system at \<^url>\<open>https://isabelle.in.tum.de/installation.html\<close>
  (including workarounds for potential issues with signatures/certificates or anti-virus
  programs).

  We recommend using the jEdit IDE, which comes bundled with Isabelle.\<close>

end