src/Doc/Tutorial/Setup.thy
author wenzelm
Sat, 02 Oct 2021 12:45:51 +0200
changeset 74410 254de9de2cd7
parent 72991 d0a0b74f0ad7
permissions -rw-r--r--
clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;

(*:maxLineLen=78:*)

theory Setup
imports Main
begin

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

end