src/Doc/Tutorial/Setup.thy

Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

(*:maxLineLen=78:*)

theory Setup
imports Main
begin

ML_file \<open>../antiquote_setup.ML\<close>
ML_file \<open>../more_antiquote.ML\<close>

end