src/HOL/Proofs.thy
author wenzelm
Mon, 15 Jul 2013 19:23:19 +0200
changeset 52663 6e71d43775e5
parent 52488 cd65ee49a8ba
permissions -rw-r--r--
retain compile-time context visibility, which is particularly important for "apply tactic";

theory Proofs
imports Pure
begin

ML "Proofterm.proofs := 2"

end