(* Title: Reference_Prerequisites.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins *) section‹Reference prerequisites› theory Reference_Prerequisites imports "HOL-Library.LaTeXsugar" begin ML_file ‹~~/src/Doc/antiquote_setup.ML› (* Copied from Transfer.thy in the main library. *) notation rel_fun (infixr "===>" 55) notation map_fun (infixr "--->" 55) end