doc-src/IsarImplementation/Thy/Base.thy
author wenzelm
Fri, 08 Oct 2010 17:41:51 +0100
changeset 39825 f9066b94bf07
parent 30272 2d612824e642
child 39846 cb6634eb8926
permissions -rw-r--r--
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX); eliminated Isar toplevel invocation functions, which belong to TTY/ProofGeneral model; moved remaining "ML toplevel" material to "Compile-time context";

theory Base
imports Pure
uses "../../antiquote_setup.ML"
begin

end